Hacker News new | comments | show | ask | jobs | submit login

Great question! So, TLA+ does have a machine-checked proof system called TLAPS, but its intended use is quite a bit different than Coq. While Coq is very well-suited for doing deep reasoning about mathematics and proving all sorts of stuff about whatever mathematical construct you care to define, TLAPS is focused much more on "mile wide, inch deep" type proofs required to demonstrate correctness of algorithms. Most algorithms use very simple mathematical properties, but have a bunch of edge cases and cyclomatic complexity which TLAPS is well-equipped to handle.

There might come a day where TLAPS is as powerful as Coq for writing general mathematical proofs (indeed, better ways of writing proofs and mathematics seem to be a passion of Dr. Lamport's, see his paper How to Write a 21st Century Proof[0]), but for now it's far, far easier to prove even simple statements about the Natural numbers in Coq.

[0] http://lamport.azurewebsites.net/pubs/proof.pdf




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact

Search: