Via the ATS mailing list:
However, there is a huge difference between mathematical proofs and programs.
A mathematical proof is often very robust in the sense that mistakes in handling minor details can likely be remedied. A popular saying is that mathematical theorems are almost always true while mathematical proofs almost always contain mistakes. On the other hand, programs are not robust at all: a typo is all you need to crash a program. The very selling point of programming-with-theorem-proving as is supported in ATS is to facilitate the construction of correct programs by taking advantage of the inherent robustness of mathematical proofs: force your programs to go through rigorous typechecking while trusting your theorems (without proofs).
Recent comments
3 hours 4 min ago
3 hours 20 min ago
3 hours 27 min ago
3 hours 38 min ago
3 hours 49 min ago
10 hours 13 min ago
10 hours 40 min ago
11 hours 9 min ago
13 hours 18 min ago
14 hours 15 sec ago