Formal methods and the future of programming
Formal methods for proving software correctness are gaining renewed attention as AI tools make it cheaper to generate vast amounts of code — and potentially to automate much of the tedious proof work. Commenters debate where rigorous specification and verification are actually worth the cost, contrasting safety‑critical domains (kernels, trading systems, cryptography) with fast‑moving product work where modeling the real world is the harder problem. Many see a near‑term future in which expressive type systems, model checkers, and proof assistants are combined with LLMs to offload low‑level reasoning, while humans focus on designing sound specifications and understanding where those specs may diverge from reality.
Role of formal methods with GenAI
- Several comments argue that GenAI is more likely to accelerate formal methods than the other way around: AI can generate tedious proofs, specs, and boilerplate.
- Idea: humans focus on high‑level specifications; LLMs generate messy code and/or proofs, with mechanical checkers ensuring correctness.
- Others note that LLM‑generated proofs and verification artifacts are currently expensive, brittle, and still require formal‑methods experts to guide them.
Cost, complexity, and limits of specifications
- Multiple posters say full formal specs for nontrivial systems are often larger and more complex than the implementation, and can be more opaque than code.
- Formal methods guarantee only consistency between spec and implementation; they do not guarantee the spec reflects reality or changing business/market conditions.
- There is concern that rigorous systems push people to “work around” them (analogized to Rust’s borrow checker), or that overly tight models just refine a wrong worldview.
Where formal methods fit (and where they don’t)
- Strong consensus that formal methods shine where semantics are crisp: kernels, protocols, parsers, compilers, crypto, concurrency primitives, hardware, safety‑critical trading.
- Many argue they are a “luxury” justified mainly in high‑risk or high‑volume domains; for startups and exploratory products, fast “offensive programming” can be more appropriate.
- Some note that even UIs and many application layers can often be modeled as state machines and benefit from specs, though top‑level UX goals remain fuzzy.
Formal methods vs tests and property‑based testing
- Key distinction: tests and property‑based testing sample behaviors; formal methods aim to prove properties for all inputs and all executions.
- However, writing precise properties can resemble implementing the function again, and subtle spec bugs (e.g., Unicode whitespace definitions, integer overflow) remain.
Tooling, languages, and workflows
- Discussion of Lean, Coq, TLA+, Dafny, SPARK/Ada, Rust verification efforts, and types-as-proofs approaches in mainstream languages.
- Several emphasize integrating specs and proofs directly into the programming language syntax to avoid “impedance mismatch.”
- Some are optimistic about emerging “spec‑driven development” and stronger type systems as a practical middle ground; others doubt formal methods will ever dominate everyday programming.