3 ms·

The confusion here is that you repeatedly seem to misunderstand my point, perhaps that is my fault as I do not have the time to write very carefully (e.g. I've

by willtim 10y ago

The confusion here is that you repeatedly seem to misunderstand my point, perhaps that is my fault as I do not have the time to write very carefully (e.g. I've used "Turing Machine" as a cheap shot at imperative programming). You even stated it yourself earlier "because our programs are most certainly not TM-equivalent". If you agree that most programs do not require Turing equivalence, then you must surely understand my main point, which is why provide powerful expressive languages that, for example, do allow Turing complete computations. Does a contract language, or even a systems language need to really support Turing completeness? You seem to argue that it doesn't matter. I think it does.

pron 10y ago
Oh, you are right that finite-state machines make automated verification easier (assuming that by Turing machine you meant Turing complete). However, some people are under the impression that other sub-Turing-complete languages (in particular, total functional programs) are easier to verify than programs in Turing-complete languages. This is false. The only class of languages that are practically "easy" to verify are finite state machines (well, if you call being PSPACE-complete easy; even that is exponential in the program's size!). This is easy to prove (in fact, it is a simple corrolary of the time hierarchy theorem and its proof). In particular, it is trivial to show that the problem of verifying a program in a total language is harder than any problem with a computable complexity bound, i.e. it's complexity is non-computable, i.e. it has "busy beaver" complexity[1]. I'm giving a talk on this precise subject next month at Curry On (http://curry-on.org/2016/sessions/why-writing-correct-software-is-hard-and-why-math-alone-wont-help-us.html http://curry-on.org/2016/sessions/why-writing-correct-softwa...) [1]: The difference, therefore, between verification of Turing-complete programs and total programs is that the cost of verifying the former in the general case is infinite, while the cost of the other grows like some function that is larger than any function we can ever compute. From the perspective of computing power, both are equally beyond reach.
- willtim 10y ago
  That looks like a great talk, I hope it will be recorded.

by willtim 10y ago

pron 10y ago

Oh, you are right that finite-state machines make automated verification easier (assuming that by Turing machine you meant Turing complete). However, some people are under the impression that other sub-Turing-complete languages (in particular, total functional programs) are easier to verify than programs in Turing-complete languages. This is false. The only class of languages that are practically "easy" to verify are finite state machines (well, if you call being PSPACE-complete easy; even that is exponential in the program's size!). This is easy to prove (in fact, it is a simple corrolary of the time hierarchy theorem and its proof). In particular, it is trivial to show that the problem of verifying a program in a total language is harder than any problem with a computable complexity bound, i.e. it's complexity is non-computable, i.e. it has "busy beaver" complexity[1]. I'm giving a talk on this precise subject next month at Curry On (http://curry-on.org/2016/sessions/why-writing-correct-software-is-hard-and-why-math-alone-wont-help-us.html http://curry-on.org/2016/sessions/why-writing-correct-softwa...) [1]: The difference, therefore, between verification of Turing-complete programs and total programs is that the cost of verifying the former in the general case is infinite, while the cost of the other grows like some function that is larger than any function we can ever compute. From the perspective of computing power, both are equally beyond reach.

willtim 10y ago
That looks like a great talk, I hope it will be recorded.