A developer shares a mental technique for writing more correct code by sketching informal proofs while coding. The post covers four key reasoning tools: monotonicity (identifying code that can only progress in one direction), pre/post-conditions (specifying constraints on function behavior), invariants (properties that must always hold), and isolation (limiting the blast radius of changes). Each concept is illustrated with practical examples, including LSM trees, double-entry accounting, and a real AST simplification function with an inductive correctness proof. The post also introduces 'proof-affinity' as a code quality metric — well-designed code is easy to reason about formally. Readers are encouraged to practice by writing mathematical proofs, taking algorithm courses, or doing LeetCode problems focused on correctness rather than tricks.
Table of contents
MonotonicityPre- and post-conditionsInvariantsIsolationInductionProof-affinity as a quality metricHow to get better at thisSort: