Hacker News Reader

Comment by mablap | Hacker News Reader

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).

View on HN

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-softwa...

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.

Reply on news.ycombinator.com