3 ms·
You should probably ask the people who've been promoting these ideas since at least the 70s :) "No time soon" is my best bet As I understand it, creating a pro
by hosay123 13y ago
You should probably ask the people who've been promoting these ideas since at least the 70s :) "No time soon" is my best bet
As I understand it, creating a proof becomes increasingly more complex in proportion to program size. You'll notice in this project, their proof only covers a few hundred lines of code. That's not because their program just happened to be a few hundred lines of code, but because they designed it to allow a practical proof.
- DebianUser 13y agoThe theory which was promoted in the 70s (whatever it was) was certainly vastly different from what's used nowadays. Thierry Coquand (who conceived the original theory behind Coq) was only 9yo. In 1970.