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

49 min 41 sec ago

14 hours 32 min ago

15 hours 46 min ago

15 hours 56 min ago

16 hours 10 min ago

16 hours 39 min ago

1 day 2 hours ago

1 day 5 hours ago

2 days 3 hours ago

4 days 1 hour ago