To be a better programmer, write little proofs in your head

Binary search and invariants as a litmus test

• Binary search (and leftmost/rightmost variants) is repeatedly cited as a case where informal reasoning fails: many “correct-looking” implementations have subtle bugs (off-by-one, infinite loops, integer overflow).
• Loop invariants are presented as the key conceptual tool to get it right; once you can express and maintain invariants, the search logic becomes much clearer.
• People mention real-world failures (standard libraries, books, interviews) and note that even professionals frequently get it wrong under time pressure.
• Some argue interview use of binary search mainly selects for LeetCode practice rather than general ability.

Proof mindset vs idiomatic simplicity

• Many commenters endorse the article’s idea: think in terms of preconditions, postconditions, invariants, induction, and “proof-affinity” of code.
• Others push back: full-on program verification is hard, and for day-to-day work, idiomatic code + good abstractions + simplicity (à la “The Practice of Programming”) often yields the necessary invariants “for free”.
• Counterargument: “clean/idiomatic” code is not a proof; clarity is a consequence of correct reasoning, not a replacement for it.

Tests, TDD, and “are tests proofs?”

• One camp sees TDD as a practical way to encode “little proofs” as executable tests, especially when combined with clear specs and types.
• Another stresses that tests are not proofs: they show behavior on sampled inputs, not all possible cases, and can easily encode incorrect assumptions.
• There’s debate over writing tests first: some find it clarifies interfaces and invariants; others feel it encourages “coding to appease tests” rather than solving the real problem.

Types, contracts, and formal methods

• Several point out that rich type systems and Curry–Howard–style thinking make “proofs in code” more natural: types as theorems, programs as proofs.
• Design-by-contract, Ada/SPARK, Rust contracts, and theorem provers are cited as ways to move proofs from your head into the language/toolchain.
• Others note mainstream ecosystems (OpenAPI/GraphQL, dynamically typed stacks) typically use weaker types and rely more on conventions and tests.

State, concurrency, and large systems

• Immutable data and constrained mutation are praised as huge aids to reasoning; global mutable state is framed as making local proofs practically impossible.
• Concurrency is called out as the domain where informal proof feels almost necessary (mutex invariants, lock-free algorithms, GC correctness).
• In large, messy codebases, commenters talk about gradually carving out “provable islands” and structuring code to make invariants visible and hard to violate.

LLMs, education, and personal practice

• Some wonder whether LLMs could be guided by proof-like checks or integrated with proof assistants instead of just emitting “plausible” code.
• Multiple people mention being taught loop invariants, induction, and formal reasoning early (or wishing they had been), and seeing it permanently change how they program.
• There’s also a pragmatic strand: you still get better mostly by writing lots of code, but using a proof mindset improves debugging, API design, and long-term maintainability.