henry_flower (![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
henry_flower) wrote2011-11-26 05:04 pm
henry_flower) wrote2011-11-26 05:04 pm
Entry tags:
В такую погоду хорошо читать про ATS http://thedeemon.livejournal.com/tag
В такую погоду хорошо читать про ATS http://thedeemon.livejournal.com/tag/ats?style=mine. Покрутив глазами, залез в эйтиэсовский mail list:
'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 type checking while trusting your theorems (without proofs).'
Здравствуй новый 1982 год.
'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 type checking while trusting your theorems (without proofs).'
Здравствуй новый 1982 год.
Permalink: https://plus.google.com/115290581164606462017/posts/F5m3BWnrRsr