5 ms·

> First, a proof that the function yields an even natural is computed (you call that type checking); second (that's the evaluation step), the actual computation

> First, a proof that the function yields an even natural is computed (you call that type checking); second (that's the evaluation step), the actual computation is carried out, and an element in the set of even numbers is computed. As stated above, not all types denote sets. For instance, in a language with general recursion, (simple) types denote domains, not sets. > But from a theoretical point of view, the total computational effort required to prove a property of a program is the same (given the same conditions), no matter when it is carried out. You are ignoring two things: (0) There is no magical way to implement the correct program if you don't have verification in mind right from the start. You will implement the wrong program, then attempt to fix it, then have another wrong program, then attempt to fix it, etc. That too has a computational cost. (1) When you design your program upfront with verification in mind, you actually have a different mathematical object than when you don't. (Just like 2 as a member of the naturals is a completely different mathematical object from 2 as a member of the reals.) If your program design is split into modules (as it should be, if your program is large enough), then enforcing abstraction barriers across module boundaries constrains the size of the design space, often dramatically. (e.g., there are too many non-parametric total functions of type `forall a. a -> a` to even form a set, but there is only one parametric such total function: the identity function.) You note that verified properties could be thrown away after the verification is done, but why would anyone in their right mind want to?

pron 10y ago
Again, you're talking about engineering. That's great, but I'm talking about theory. You're saying that it's easier to build a building from the bottom upwards -- and that's true -- but theoretically a building would be just as strong if it were somehow built from the top down. Of course, no one would think to build skyscraper starting from the top, but that doesn't mean that the theory of structure must always incorporate the study of construction. I'm not talking about the process of construction, but the properties of the structure. I'm not arguing with any of what you've said here, simply talking about different aspects. Keep in mind that not all computational process -- certainly not all studied in TOC -- are programmed by humans at all. 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. This means that there's value in studying the problem of verification even separately from the study of programming. Indeed, this is how it has mostly been done in academia. The software verification community uses very different concepts from the PLT community, concepts that are much closer to abstract machine models than to language models.
- catnaroek 10y ago
  > 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.

pron 10y ago

Again, you're talking about engineering. That's great, but I'm talking about theory. You're saying that it's easier to build a building from the bottom upwards -- and that's true -- but theoretically a building would be just as strong if it were somehow built from the top down. Of course, no one would think to build skyscraper starting from the top, but that doesn't mean that the theory of structure must always incorporate the study of construction. I'm not talking about the process of construction, but the properties of the structure. I'm not arguing with any of what you've said here, simply talking about different aspects. Keep in mind that not all computational process -- certainly not all studied in TOC -- are programmed by humans at all. 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. This means that there's value in studying the problem of verification even separately from the study of programming. Indeed, this is how it has mostly been done in academia. The software verification community uses very different concepts from the PLT community, concepts that are much closer to abstract machine models than to language models.

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