3 ms·

assuming the entirety of centuries of civilization has no clue what they were doing This is a common assumption in these circles, unfortunately.

by mablap 10y ago

pron 10y ago
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.
- 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.

assuming the entirety of centuries of civilization has no clue what they were doing This is a common assumption in these circles, unfortunately.

by mablap 10y ago

assuming the entirety of centuries of civilization has no clue what they were doing This is a common assumption in these circles, unfortunately.

pron 10y ago

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.

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.