4 ms·
Provable Programming provably requires non-Turing-complete languages. Which isn't an insuperable barrier, to be sure, but it's a big piece of evidence against
by derleth 14y ago
Provable Programming provably requires non-Turing-complete languages.
Which isn't an insuperable barrier, to be sure, but it's a big piece of evidence against its practicality in actual commercial environments.
- ibotty 14y agowhy has this been downvoted? if this is wrong, a simple "no, this is wrong. see e.g. blah" would have been nice.
- daivd 14y agoDiagonal proofs like the Halting Problem say that in general you can not prove properties about all programs in a Turing complete language. Thus, there is a class of troublesome programs. Likewise there is obviously a great number of programs in Turing complete languages that you can prove properties about. Thus, there is a class of pleasant programs (or [program, property] pairs). We do not know for certain how many of the programs that we want to write that is in each class. I would venture a guess that >99% of all programs ever written are in the "nice" class. If it is really impossible to reason about some property of a program, why would you think it works?