Blog
Here I write about formal methods, low-level and concurrent systems, and anything else I might find interesting.
Series
- Reactive Programming in Lean
- Proving the Coding Interview (Lean 4)
- Let's Build a Theorem Prover
- Proving the Coding Interview (Dafny)
All posts
- FRP in Lean: Stateful combinators, safety, and liveness
- FRP in Lean: Events and LTL.eventually If Signals type to LTL.always, what could type to LTL.eventually?
- FRP in Lean: Reactive Signals and LTL.always So if propositions are types, and LTL are propositions, what programs are well-typed by LTL?
- Reactive Programming in Lean Part 3: Linear Temporal Logic Specifications that move through time
- Reactive Programming in Lean Part 2: Execution traces Recording and reasoning about the states our programs pass through
- Reactive Programming in Lean 4 Extending Lean's dependent type system to reason about reactive programs
- Leaning into the Coding Interview 4: Certified Programming with Proof-Carrying Code Migrating from `List` to `Vector` paid dividends for us being convinced that our Fizzbuzz implementation was correct. Does making our `FB` value type dependent also increase our confidence of correctness?
- Leaning into the Coding Interview: proving equality of different Fuzzbuzzes There are lots of different ways to implement Fizzbuzz but this one is mine - how can we prove different implementations are actually the same, and what does it look like when they're actually not?
- Leaning into the Coding Interview 3: completing our spec with tacticals and metaprogramming Time to actually write our end-to-end specification!
- Leaning Into the Coding Interview 2: static bounds checks and dependent types Pls types? No terms! Only (indexed, dependent) types!
- Leaning Into the Coding Interview: Lean 4 vs Dafny cage-match Is Fizzbuzz easier to write in Lean, or just differently hard?
- An Invitation to Liquid Types: Unifying Type Theory and Model Checking
- Let's Build a Theorem Prover: Lazy and Basic? SAME Implementing the lazy CDCL(T) algorithm with Union-Find for equality reasoning
- Let's Build a Theorem Prover: SMT 2: Not(Eq(urne)) Lazy SMT solving: building an SMT solver with iterative refinement and blocking lemmas
- Let's Build A Theorem Prover: Satisfiability Modulo Theory: Digital Deduction Saga From propositional logic to first-order logic: introducing theories and equality reasoning into SAT solvers
- Let's Build a Theorem Prover: SATvatar 2: the way of solver From Davis-Putnam to DPLL to CDCL: improving SAT solvers with backtracking and conflict-driven clause learning
- Let's Build a Theorem Prover: Decision procedure lifestyle trends The president has ordered all programmers to maximise their automated reasoning with these weird tricks! Logical agents hate this!
- Proving the Coding Interview: verifying the JDK's `Integer.toString()` A faster, but just as correct, nat -> string converter
- Proving the Coding Interview II Integer.toString() 2 furious
- Notes on setting up Ivy in Python 3
- Proving the Coding Interview Applying interesting research to uninteresting interview problems