3 ms·

Yes! I read a great comment here (I forgot by whom) that said something like It's hard enough to prove that a computer program will actually do somet

by mablap 10y ago

Yes! I read a great comment here (I forgot by whom) that said something like It's hard enough to prove that a computer program will actually *do* something, forget about proving what the program *will not* do. He was arguing against the idea that Turing complete languages should be used in smart contracts. The person mentioned that it's not trivial to even assign a complexity category to the question asked, let alone getting an answer (if you can).

pron 10y ago
Right, although "Turing complete" is a red herring here, as we can't generally verify the behaviors of programs written in most non-Turing complete languages either. I wrote in another comment that if we place computational power on a scale and put Turing completeness at 10 and FSM at 1 (0 being no computation at all, i.e, return the input), then the computational power that we can always generally verify would lie somewhere between 0 and 1. Even FSMs are PSPACE-complete to verify, meaning we can only generally verify small ones (which is why software verification isn't about finding a language in which all programs are tractably verifiable -- as it is unlikely that such a language would be very useful -- but rather to try and verify specific programs that form a small subset of all possible program, regardless of the computational model of the language they're written in). So the general intractability of computation is essential and far from limited to Turing completeness. If you find this subject interesting, I'll be giving a talk about it next month[1] (it will be recorded). [1]: 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...
- mablap 10y ago
  Cool, I am indeed interested. I read Aaronson's "Quantum Computing Since Democritus" and enjoyed it, but that's the only source I read concerning computational complexity.

Yes! I read a great comment here (I forgot by whom) that said something like It's hard enough to prove that a computer program will actually *do* somet

by mablap 10y ago

pron 10y ago

Right, although "Turing complete" is a red herring here, as we can't generally verify the behaviors of programs written in most non-Turing complete languages either. I wrote in another comment that if we place computational power on a scale and put Turing completeness at 10 and FSM at 1 (0 being no computation at all, i.e, return the input), then the computational power that we can always generally verify would lie somewhere between 0 and 1. Even FSMs are PSPACE-complete to verify, meaning we can only generally verify small ones (which is why software verification isn't about finding a language in which all programs are tractably verifiable -- as it is unlikely that such a language would be very useful -- but rather to try and verify specific programs that form a small subset of all possible program, regardless of the computational model of the language they're written in). So the general intractability of computation is essential and far from limited to Turing completeness. If you find this subject interesting, I'll be giving a talk about it next month[1] (it will be recorded). [1]: 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...

mablap 10y ago
Cool, I am indeed interested. I read Aaronson's "Quantum Computing Since Democritus" and enjoyed it, but that's the only source I read concerning computational complexity.