Formal methods and the future of programming

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.