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

20 min 18 sec ago

3 hours 51 min ago

5 hours 36 min ago

6 hours 37 min ago

7 hours 57 min ago

8 hours 3 min ago

10 hours 2 min ago

13 hours 44 min ago

13 hours 56 min ago

1 day 6 hours ago