9 ms·

> Again, you're talking about engineering. No, I'm not. I'm talking about math. (If you read my comment history, my distaste for “engineering” should be obviou

> Again, you're talking about engineering. No, I'm not. I'm talking about math. (If you read my comment history, my distaste for “engineering” should be obvious, at least if by “engineering” we mean “software engineering”.) > but theoretically a building would be just as strong if it were somehow built from the top down. The amount of mental gymnastics required to produce this statement (not to mention expect someone else to believe it) completely baffles me. > Computational processes in a living cell, for example, also have to ensure correctness -- and therefore spend computational resources on "verification" -- yet they don't use symbolic logic for that task. Nature doesn't do “verification”, because there's no specification in the first place. Nature just evolves a variety of systems, and those that aren't fit enough to survive, well, just die. Also, the evolution of biological systems happens way too slowly to use it as inspiration for how to design computational systems for our own purposes.

pron 10y ago
> No, I'm not. I'm talking about math. Good. In that case, verifying that a program conforms to spec in the general case is of as much computational complexity no matter when it's carried out. This is proven and well known. For an overview, you can see my post here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... In short, the reason for that is that the every computational problem with a computable upper bound on complexity can be efficiently reduced to verification. The complexity required to verify is a function of the spec, and can be made arbitrarily hard. > The amount of mental gymnastics required to produce this statement (not to mention expect someone else to believe it) completely baffles me. OK, so let me use another analogy. That you can wind up a wind-up toy before I enter the room doesn't mean that just because you hid that from me, the toy requires any less external energy to run than when you'd wind it at any other time. Discussions of ergonomic ways to wind the toy (with a larger lever perhaps) may be interesting, but they're separate from this basic fact. Verification is a computational problem, and one of a certain complexity. That complexity must be paid, no matter what, no matter when. The knowledge that a certain program has a certain property has a price-tag, and there are no discounts. Because all computational problems efficiently reduce to verification, if you believe you've found a loophole, I could use it to solve much bigger problems than ensuring that your recipe application is correct. > Nature doesn't do “verification”, because there's no specification in the first place. Nature just evolves a variety of systems, and those that aren't fit enough to survive, well, just die. You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce. Computational complexity results are used in the study of biological systems. Look at the work by Leslie Valiant (Turing award) or Stuart Kauffman (https://en.wikipedia.org/wiki/Stuart_Kauffman https://en.wikipedia.org/wiki/Stuart_Kauffman). Incidentally, TLA+ can also be used to model systems such as metabolic pathways, as those are very easily described as nondeterministic state machines: http://www.cosbi.eu/research/publications?pdf=5437 http://www.cosbi.eu/research/publications?pdf=5437 > Also, the evolution of biological systems happens way too slowly to use it as inspiration for how to design computational systems for our own purposes. Maybe, but TOC doesn't study how to design computational systems for our own purposes. It's pure science. If its discoveries turn out to be useful, then that's a happy coincidence. For that matter, neither does most of TOP for the past couple of decades or so. If you do math to study a system designed for use by a computationally-complex collaborator (the programmer in this case), you must study the collaborator as well. TOP shows no interest in such empirical study, and has therefore been utterly unable to prove that the approaches it advocates actually help write very large complex software systems; indeed it has been even unwilling to test this hypothesis, not even once.
- catnaroek 10y ago
  > In that case, verifying that a program conforms to spec in the general case is of as much computational complexity no matter when it's carried out. Then, as Dijkstra said, don't focus on the general case: “So, instead of trying to devise methods for establishing the correctness of arbitrary, given programs, we are now looking for the subclass of "intellectually manageable programs", which can be understood and for which we can justify without excessive amounts of reasoning our belief in their proper operation under all circumstances.” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD288.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E... > The knowledge that a certain program has a certain property has a price-tag, and there are no discounts. So what? If you're designing programs out of reusable components and you don't throw away their proofs of correctness, then much of the cost has already been paid by someone else before you even start. > You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce. This still doesn't make sense. No biological system is “correct” in any meaningful sense. Correctness is always relative to a specification, and, even if your specification is as vague as “survive”, what's happening in nature is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones.
  - pron 10y ago
    > Then, as Dijkstra said, don't focus on the general case Exactly, except that since Dijkstra gave that talk (early seventies) we have learned some important results in computational complexity. The bottom line is that we know that it is impossible to create a generally useful programming language (even not Turing-complete; even a finite-state machine) where every program is relatively cheap to verify (in 2000 it was proven that language abstractions can't significantly reduce verification cost even though it would have been reasonable to believe that they could; that result is discussed in my linked post). Whatever language is chosen, only a small subset of programs written in that language will be verifiable. Identifying that subset requires extensive empirical research. This is done in the software verification community; unfortunately the PL community is reluctant to conduct empirical research. > much of the cost has already been paid by someone else before you even start. Not true. See the Schnoebelen results quoted in my post that I linked to. Composing proofs of program correctness requires proof effort that is intractable in the complexity of each component, not in the number of components. This was proven in 2005. In technical terms, verification isn't Fixed-Parameter Tractable, or FPT, a relatively modern[1] complexity class created to incorporate problems that are intractable in the general case but may be tractable in practice. In simple terms, that each of your components has been proven correct still means that the difficulty of proving the composite's correctness is an intractable function (exponential at least) in the complexity of each component. Of course, theoretically it's better than nothing, but not by enough. > is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones. That is only if you view each life form as the computational system. However, that genetic algorithm I was referring to is conducted by all living systems as a single computational system. [1]: https://en.wikipedia.org/wiki/Parameterized_complexity https://en.wikipedia.org/wiki/Parameterized_complexity

pron 10y ago

> No, I'm not. I'm talking about math. Good. In that case, verifying that a program conforms to spec in the general case is of as much computational complexity no matter when it's carried out. This is proven and well known. For an overview, you can see my post here: http://blog.paralleluniverse.co/2016/07/23/correctness-and-complexity/ http://blog.paralleluniverse.co/2016/07/23/correctness-and-c... In short, the reason for that is that the every computational problem with a computable upper bound on complexity can be efficiently reduced to verification. The complexity required to verify is a function of the spec, and can be made arbitrarily hard. > The amount of mental gymnastics required to produce this statement (not to mention expect someone else to believe it) completely baffles me. OK, so let me use another analogy. That you can wind up a wind-up toy before I enter the room doesn't mean that just because you hid that from me, the toy requires any less external energy to run than when you'd wind it at any other time. Discussions of ergonomic ways to wind the toy (with a larger lever perhaps) may be interesting, but they're separate from this basic fact. Verification is a computational problem, and one of a certain complexity. That complexity must be paid, no matter what, no matter when. The knowledge that a certain program has a certain property has a price-tag, and there are no discounts. Because all computational problems efficiently reduce to verification, if you believe you've found a loophole, I could use it to solve much bigger problems than ensuring that your recipe application is correct. > Nature doesn't do “verification”, because there's no specification in the first place. Nature just evolves a variety of systems, and those that aren't fit enough to survive, well, just die. You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce. Computational complexity results are used in the study of biological systems. Look at the work by Leslie Valiant (Turing award) or Stuart Kauffman (https://en.wikipedia.org/wiki/Stuart_Kauffman https://en.wikipedia.org/wiki/Stuart_Kauffman). Incidentally, TLA+ can also be used to model systems such as metabolic pathways, as those are very easily described as nondeterministic state machines: http://www.cosbi.eu/research/publications?pdf=5437 http://www.cosbi.eu/research/publications?pdf=5437 > Also, the evolution of biological systems happens way too slowly to use it as inspiration for how to design computational systems for our own purposes. Maybe, but TOC doesn't study how to design computational systems for our own purposes. It's pure science. If its discoveries turn out to be useful, then that's a happy coincidence. For that matter, neither does most of TOP for the past couple of decades or so. If you do math to study a system designed for use by a computationally-complex collaborator (the programmer in this case), you must study the collaborator as well. TOP shows no interest in such empirical study, and has therefore been utterly unable to prove that the approaches it advocates actually help write very large complex software systems; indeed it has been even unwilling to test this hypothesis, not even once.

catnaroek 10y ago
> In that case, verifying that a program conforms to spec in the general case is of as much computational complexity no matter when it's carried out. Then, as Dijkstra said, don't focus on the general case: “So, instead of trying to devise methods for establishing the correctness of arbitrary, given programs, we are now looking for the subclass of "intellectually manageable programs", which can be understood and for which we can justify without excessive amounts of reasoning our belief in their proper operation under all circumstances.” https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD288.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/E... > The knowledge that a certain program has a certain property has a price-tag, and there are no discounts. So what? If you're designing programs out of reusable components and you don't throw away their proofs of correctness, then much of the cost has already been paid by someone else before you even start. > You're wrong because, again, you're blind to computational complexity and to computational processes that aren't man-made programs. What you described is precisely how nature computes. That things that aren't fit enough to survive "just die" is a verification process by a genetic algorithm (that requires tremendous time and space complexity) to conform with the spec for genes -- i.e. life's "software" -- which is: reproduce. This still doesn't make sense. No biological system is “correct” in any meaningful sense. Correctness is always relative to a specification, and, even if your specification is as vague as “survive”, what's happening in nature is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones.
- pron 10y ago
  > Then, as Dijkstra said, don't focus on the general case Exactly, except that since Dijkstra gave that talk (early seventies) we have learned some important results in computational complexity. The bottom line is that we know that it is impossible to create a generally useful programming language (even not Turing-complete; even a finite-state machine) where every program is relatively cheap to verify (in 2000 it was proven that language abstractions can't significantly reduce verification cost even though it would have been reasonable to believe that they could; that result is discussed in my linked post). Whatever language is chosen, only a small subset of programs written in that language will be verifiable. Identifying that subset requires extensive empirical research. This is done in the software verification community; unfortunately the PL community is reluctant to conduct empirical research. > much of the cost has already been paid by someone else before you even start. Not true. See the Schnoebelen results quoted in my post that I linked to. Composing proofs of program correctness requires proof effort that is intractable in the complexity of each component, not in the number of components. This was proven in 2005. In technical terms, verification isn't Fixed-Parameter Tractable, or FPT, a relatively modern[1] complexity class created to incorporate problems that are intractable in the general case but may be tractable in practice. In simple terms, that each of your components has been proven correct still means that the difficulty of proving the composite's correctness is an intractable function (exponential at least) in the complexity of each component. Of course, theoretically it's better than nothing, but not by enough. > is that some life forms are lucky enough to be fit for their current circumstances, not all possible ones. That is only if you view each life form as the computational system. However, that genetic algorithm I was referring to is conducted by all living systems as a single computational system. [1]: https://en.wikipedia.org/wiki/Parameterized_complexity https://en.wikipedia.org/wiki/Parameterized_complexity