tags : Math, Concurrency, Algorithms

## Intro

- Different formalisms often have different ergonomics when it comes to different particular systems and properties, and the matter of personal aesthetic preference also plays a big role.
- At the end of the day, many those formalisms have similar expressivity (i.e., they can describe roughly the same set of systems and the same set of properties)

## Theorem Provers and Formal Spec Tools

- Formal Logic :
`formal specification (description)`

+`formal proof`

- Writing
`formal specification`

is different skillset from writing`formal proofs`

. - You can write
`formal specification`

without knowing how to write`formal proof`

Name | Type |
---|---|

Alloy | Spec Tool |

TLA+ | Spec Tool |

Z3 | Model Checker |

Lean | Proof Writing |

Coq | Proof Writing |

Isablle | Proof Writing |

### Formal specification first

#### Temporal Logic of Action(TLA+)

- Good for specification of
`order`

- TLA+ is a modelling/specification language for computational processes.
- Lamport’s hypothesis was that a programming language, no matter how simple, is still much more complicated and far less expressive than simple mathematics.
- Time is viewed as discrete (rather than continuous), considers branching time (as opposed to linear time) and in which time branches only into the future (and not into the past).
- Can be use to prove Paxos and Raft
- Can support Model checkers like Z3
- Resources
- An introduction to temporal logic and how it can be used to analyze concurrency | Hacker News
- An Introduction to TLA+ and Its Use in Parties | Lobsters
- Using TLA+ in the Real World to Understand a Glibc Bug
- TLA+ in Practice and Theory<br/>Part 1: The Principles of TLA+
- A primer on formal verification and TLA+ — Jack Vanlightly
- Wrangling monotonic systems in TLA (See crdt)

#### Alloy

- Good for specification of
`structure`

- Resources

### Proof writing first

Lean and Coq are based on Lambda calculus

#### Lean

- Lean is a FP language and theorem prover that compiles to C
- Lean’s maths library is completely focused on classical mathematics
- From Z3 to Lean, Efficient Verification
- Logic and Proof — Logic and Proof 3.18.4 documentation

#### Coq

- Theorem Prover, Proof Assistant
- Learn Coq in Y Minutes

### Model Checkers

#### SMT Solvers

Satisfiability Modulo Theories Solver

- SAT/SMT by Example (Book, Z3py)
- First-order logic - Wikipedia
- Learning 1: Reddit - Dive into anything
- Learning 2: Reddit - Dive into anything

#### Z3

## Resources

- Formal Methods: Just Good Engineering Practice? - Marc’s Blog
- What I’ve Learned About Formal Methods In Half a Year — Jakob’s Personal Webpage
- PWLSF - 08/2014 - Peter Alvaro: Using Reasoning about Knowledge to Analyze Di…
- Logic and Algebras for Distributed Computing: Applications and Open Questions…