A tour of the massive collection of things I think you should know about in formal methods.
Here's what I plan to cover
- Famous paradoxes, totality, computability, intro to logics, Gödel, Church, and Turing,
- Type Theory. Building up to CiC (Calculus of Inductive Constructions) from untyped lambda calculus,
- A deservedly long tour of proof assistants: Coq, Isabelle, Idris, Agda, Lean,
- A quick tour of model checking and SMT solvers,
- A quick tour in the recent efforts in formal verification.
- A real treatment of verifying something system level. Rust and Separation logic likely involved.
- A real treatment of verifying something cryptography. Algebra involved, Cryptol + Saw likely involved.
- A real treatment of verifying something hardware. SystemVerilog likely involved.
The earlier writings focuses on the "why"s: Why do want dependent types? Why do we have so many proof assistants? The later writings start to zoom-in on the "how"s.
I hope that when you see this, I have a few crisp chapters done. But it will be a long journey for me. Out of the eight sections I planned, I am only confident in writing about the first two with my current knowledge. But, this is my profession, so I get the chance to sit in it all day, and I will sure slay the beast.
Reminders to self:
- A concept is useless without examples,
- Put myself in it sometimes — how did I learn X?