- Author
- Posted by eatonphil, with replies from many commenters
- Published
- 29 June 2026
- Kind
- Hacker News discussion thread
- Original
- news.ycombinator.com/item?id=48719521
- Subject
- Formal methods and proof
What it is
Posted by eatonphil, the thread links an ACM Queue article about what developers can guarantee. Commenters quote the article saying a verified core leaves the database and interface outside. The thread is a discussion, not a study.
What it says
- The commenter dfabulich says formal verification suits few app developers. E-commerce code, the comment argues, is mostly input and output.
- The commenter dfabulich calls verification a speed-up for property-based testing. Testing fuzzes a rule; verification proves it always holds.
- The commenter gf000 says a model can treat a database call as succeeding or failing. The rest of the code can then be verified against that assumption.
- The commenter jongjong argues that a spec must be as detailed as the code. Writing it down correctly is as hard as writing the code.
- The commenter pron doubts that using AI makes proofs cheaper. Any cost multiplier for humans may stay the same for a model.
- The commenter derdi says verifiers demand proofs of termination and safe access without any spec. The commenter agentultra suggests model checking instead of full proofs.
- The commenter tikhonj reports that property-based testing found bugs in database-heavy apps. The same commenter used properties to agree on metrics with a planning team.
What evidence it gives
The thread offers opinion and anecdote from commenters. One recalls a college project on Lamport's bakery algorithm. Another describes a supply chain simulation at Target. Another cites a paper on testing Spotify and YouTube web APIs. No commenter gives measurements of verification cost.
Interests and limits
The ACM Queue article was blocked by a Cloudflare check; only the thread was read. The article's claims here come only from what commenters quote. Commenters are unverified. Some promote their own tools, such as a metaparsing project and a verified web frontend.