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

12 hours 14 min ago

12 hours 25 min ago

13 hours 26 min ago

17 hours 58 min ago

19 hours 15 min ago

20 hours 14 min ago

20 hours 51 min ago

22 hours 18 min ago

23 hours 49 min ago

1 day 16 min ago