Comment by pron | Hacker News Reader

Comment by pron | Hacker News Reader

Parent Full thread

I think that there is an interesting outlook here. It seems to me that some people are under the impression that the world is essentially simple, and it is stupid people and institution that complicate it. If we apply careful mathematical reasoning, we could find better solutions to anything.

The interesting thing is that about 100 years ago some mathematicians believed something similar about math itself. They believed that since we have formal procedures to reason about math, eventually we'd be able to understand (i.e. prove) everything we want to know. That hope was finally crushed by the discovery of simple, finite, small mathematical objects, that while subject to mathematical reasoning, are able to forever elude complete understanding and proof. Those objects inhabit a very large, unbridgeable gap between our ability to reason and our ability to fully understand (and prove). Those objects, of course, are what today we call computer programs.

If there's anything that proves beyond any doubt that even systems that operate according to a small set of rules, and subject to mathematical reasoning and manipulation, are still able to defy complete understanding -- even in theory, let alone in practice -- it is computer science.

Yet, even though computer science is the very discipline that proved that complexity that can arise even in the smallest of systems is essential and cannot ever be tamed, it is computer scientists and software developers who often attempt to challenge the very foundation of their own discipline.

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

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