4 ms·

> Again, no one in the history of humanity has managed to do this affordably for programs of significant size. If you have, you are pretty much guaranteed a Tur

by User23 6y ago

> Again, no one in the history of humanity has managed to do this affordably for programs of significant size. If you have, you are pretty much guaranteed a Turing award. I offer that perhaps the issue here is an ignorance of the history of humanity, at least with respect to computing? You have heard of decomposing a large program into smaller programs, right? That's how it is done and has been done. Dijkstra did do what you claim is impossible several times in his career, for example the THE multiprogramming system. And he did win a Turing award for doing so[1]. He also had more than a few colleagues and students over the years and at least some learned what he was awarded for. Of course if you're going to move the goalposts such that it having been done means the problem isn't of "significant size" then I'm happy to dismiss your argument as sophistry. > Formal mathematics is not necessarily checked by a computer, but it is necessarily checkable by a computer. Irrelevant to my point. And human programmers routinely derive programs specified to cause pathological behavior in checkers, which is to say making them impracticable to check. > That's not the point. The point of formal methods is not to do the things we know how to do, but to do things we're not sure we know how to do. This is a foolish self-imposed constraint. The point of formal mathematical reasoning is to be unambiguous, to reduce cognitive load by letting the symbols do as much of the work as possible, and to be confident in the result arrived at. This is just as useful for solving known problems[1] as it is for researching novel algorithms. And as I'm sure you'd agree there are plenty of concurrency problems that are solved in the literature but are still tricky to implement correctly even given a formal specification. Formal mathematical reasoning, for example using predicate transformers to derive a program text that satisfies the specification, is a good way to keep that trickiness within the capabilities of those of us who are not Von Neumann tier intellectual powerhouses, but are at least bright enough to manage the predicate calculus. > Your claim is mathematically disproven by the proof I've given. This isn't an argument, but a mathematical result: program verification is reducible to synthesis. You didn't at all prove that, but I trust you that reducibility of verification to synthesis has been proved[3]. It's still irrelevant to my claim about it being easier for a programmer to derive programs that meet an arbitrary specification than to test that an arbitrary program text satisfies it. Human programmers aren't computers. Please stop misrepresenting my claims. Are you one of those philosophical types who believes that human beings are turing machines? That would certainly explain your confusion and the persistent disconnect in our views. [1] https://amturing.acm.org/award_winners/dijkstra_1053701.cfm https://amturing.acm.org/award_winners/dijkstra_1053701.cfm [2] Most working programmers can't even implement binary search correctly, to say nothing of writing a correct lock-free queue or similar. [3] That's less interesting than it sounds. Given a working verifier we can just enumerate all strings and return the first one the verifier accepts. Obviously the complexity of the verification dominates and the synthesis will fall within the same computational complexity class.

pron 6y ago
> I offer that perhaps the issue here is an ignorance of the history of humanity, at least with respect to computing? Perhaps, but as no one has offered a counterexample, I have no way of knowing. > Dijkstra did do what you claim is impossible several times in his career No, he did not. The meaning of a technique not being scalable is that while it does work for small instances it does not for large ones. We have learned so much since Dijkstra, and can apply even more powerful end-to-end verification/synthesis than he had at his disposal and for larger programs, but we still can't scale it, just as he couldn't, and, indeed, didn't. > You have heard of decomposing a large program into smaller programs, right? That's how it is done and has been done. No, it has not been done, but unlike 50 years ago, in the decades we've studied the "hardness" of program analysis/synthesis we have an idea as to why. There are now complexity theory results that show that decomposition cannot always work. In addition, we now know -- what we didn't 50 years ago -- that there are essential barriers to scaling. Things that are easy when small can be absolutely impossible when large. > This is a foolish self-imposed constraint. It's not a constraint as much as saying that the claim you have a technique that can more effectively yield programs that we already know how to get more-or-less right and the claim you have a technique that can effectively, feasibly and scalably produce programs that are otherwise very hard to get right are two very different claims. It's like the difference between improving a polynomial algorithm by a constant and finding a polynomial algorithm for NP-complete problems. The first might get you published; the second will make you world-famous. > It's still irrelevant to my claim about it being easier for a programmer to derive programs that meet an arbitrary specification than to test that an arbitrary program text satisfies it. The proof is relevant because it precisely proves that your claim, as stated, is, in fact, false. Your claim might be made about "common cases" etc., but that would require a much more careful wording, as well as a careful empirical study rather than insistence.
- User23 6y ago
  > No, he did not. The meaning of a technique not being scalable is that while it does work for small instances it does not for large ones. I see, so a complete and correct multiprocessing operating system running on unreliable hardware is a "small instance" according to you. This is the sophistry I promised to dismiss. Consider it done. > There are now complexity theory results that show that decomposition cannot always work. Obviously decomposition can't always work. Primitives can't be decomposed by definition. Yet another trivial truth. >It's not a constraint as much as saying that the claim you have a technique that can more effectively yield programs that we already know how to get more-or-less right and the claim you have a technique that can effectively, feasibly and scalably produce programs that are otherwise very hard to get right are two very different claims. It's like the difference between improving a polynomial algorithm by a constant and finding a polynomial algorithm for NP-complete problems. The first might get you published; the second will make you world-famous. This word-salad has nothing to do with anything I've written. > The proof is relevant because it precisely proves that your claim, as stated, is, in fact, false. Your claim might be made about "common cases" etc., but that would require a much more careful wording, as well as a careful empirical study rather than insistence. This is more interesting, but also misleading. Obviously every single program ever written falls within the class of "common cases," since, asymptotically speaking, very nearly all program texts have never been written, let alone studied. Look ma, I can do sophistry too!

by User23 6y ago

pron 6y ago

> I offer that perhaps the issue here is an ignorance of the history of humanity, at least with respect to computing? Perhaps, but as no one has offered a counterexample, I have no way of knowing. > Dijkstra did do what you claim is impossible several times in his career No, he did not. The meaning of a technique not being scalable is that while it does work for small instances it does not for large ones. We have learned so much since Dijkstra, and can apply even more powerful end-to-end verification/synthesis than he had at his disposal and for larger programs, but we still can't scale it, just as he couldn't, and, indeed, didn't. > You have heard of decomposing a large program into smaller programs, right? That's how it is done and has been done. No, it has not been done, but unlike 50 years ago, in the decades we've studied the "hardness" of program analysis/synthesis we have an idea as to why. There are now complexity theory results that show that decomposition cannot always work. In addition, we now know -- what we didn't 50 years ago -- that there are essential barriers to scaling. Things that are easy when small can be absolutely impossible when large. > This is a foolish self-imposed constraint. It's not a constraint as much as saying that the claim you have a technique that can more effectively yield programs that we already know how to get more-or-less right and the claim you have a technique that can effectively, feasibly and scalably produce programs that are otherwise very hard to get right are two very different claims. It's like the difference between improving a polynomial algorithm by a constant and finding a polynomial algorithm for NP-complete problems. The first might get you published; the second will make you world-famous. > It's still irrelevant to my claim about it being easier for a programmer to derive programs that meet an arbitrary specification than to test that an arbitrary program text satisfies it. The proof is relevant because it precisely proves that your claim, as stated, is, in fact, false. Your claim might be made about "common cases" etc., but that would require a much more careful wording, as well as a careful empirical study rather than insistence.

User23 6y ago
> No, he did not. The meaning of a technique not being scalable is that while it does work for small instances it does not for large ones. I see, so a complete and correct multiprocessing operating system running on unreliable hardware is a "small instance" according to you. This is the sophistry I promised to dismiss. Consider it done. > There are now complexity theory results that show that decomposition cannot always work. Obviously decomposition can't always work. Primitives can't be decomposed by definition. Yet another trivial truth. >It's not a constraint as much as saying that the claim you have a technique that can more effectively yield programs that we already know how to get more-or-less right and the claim you have a technique that can effectively, feasibly and scalably produce programs that are otherwise very hard to get right are two very different claims. It's like the difference between improving a polynomial algorithm by a constant and finding a polynomial algorithm for NP-complete problems. The first might get you published; the second will make you world-famous. This word-salad has nothing to do with anything I've written. > The proof is relevant because it precisely proves that your claim, as stated, is, in fact, false. Your claim might be made about "common cases" etc., but that would require a much more careful wording, as well as a careful empirical study rather than insistence. This is more interesting, but also misleading. Obviously every single program ever written falls within the class of "common cases," since, asymptotically speaking, very nearly all program texts have never been written, let alone studied. Look ma, I can do sophistry too!