4 ms·

> Fortunately Fields Medal tier mathematical problems have never come up in my professional programming career. Ah, but you see, I've used this problem only be

by pron 6y ago

> Fortunately Fields Medal tier mathematical problems have never come up in my professional programming career. Ah, but you see, I've used this problem only because you could be easily convinced of its difficulty because it's a well-known one and others have tried solving it unsuccessfully. But hard problems come up all the time, especially when concurrency is involved. You just don't know they're hard at first glance. For example, the specification that a database be kept on multiple computers to offer redundancy without loss of data is a staple of distributed computing, but finding an algorithm that does it (perhaps together with some other latency requirements) is extremely hard and it took many years to find the first one that could do it. That easy specifications are easy to derive doesn't help us, because they might also be the same programs that are easy to test or be convinced of their correctness in some other ways. The whole point of formal methods is to help us with the hard cases, which, sadly, are very frequent. > A program can feasibly be derived that can't feasibly be verified without access to the discrete documented steps of the derivation. Not if it's done formally. A formal derivation guarantees proof, and, in fact, the problem of verification is easily reducible to derivation, i.e., derivation is no easier. Here is the proof: X is a program, and so, also a specification, and P(X) is some property that you want to verify for X. A formal derivation of a program from the specification X ∧ P(X) will, therefore, prove P(X). This is the "trick" I used with the "Goldbach program", except it's not a trick, but a basic result in the study of the hardness of program analysis, a subject that's been extensively studied for a few decades now. The claim that it's easier to derive than to prove is just mathematically false. With regards to claims about informal "proofs" or "derivations" it's hard to say anything, because the problem is not well-stated.

User23 6y ago
> finding an algorithm that does it (perhaps together with some other latency requirements) is extremely hard and it took many years to find the first one that could do it. I agree. And correctly implementing those algorithms is much easier using a formal derivation with a mathematical tool such as the predicate calculus than it is by just eyeballing it and hoping your tests catch all errors. > But hard problems come up all the time, especially when concurrency is involved Predicate transformers are well suited for reasoning about nondeterminism and concurrency. > Not if it's done formally Program derivation with predicate transformers is done formally. It's a chain of equivalences, implications, and consequences as appropriate to the problem. The program text is literally developed as a proof, and each transformation of the code must be justified by axiom, theorem, or lemma and at the end of that derivation all properties of the specification hold. You can't possibly be claiming that no formal mathematics was done before the invention of automated checkers, because that would be both ridiculous and observably false. > Here is the proof: X is a program, and so, also a specification, I disagree. A specification maps to either an empty or countably infinite set of programs that satisfy it. Also all programs satisfy countably infinitely many specifications. They are not isomorphic or even dual. In this case that conflation doesn't seem to impair our understanding too much though. > and P(X) is some property that you want to verify for X. Right, and the task of the programmer is to write a program text that provably establishes that P(X) holds everywhere in the program state space. > A formal derivation of a program from the specification X ∧ P(X) will, therefore, prove P(X) Yes this is what I meant when I said you should use the same techniques to derive the program text that you would to derive any other mathematical proof. > it's not a trick, but a basic result in the study of the hardness of program analysis It's a trick because it's a clever way of saying write a program for which there is no known algorithm. As of now nobody is going to be able to do that regardless of their methodology. I get the impression that you mean this to be a compelling point, but I'm not grasping how I'm better off not using mathematical reasoning to derive the programs that I do know how to write. > The claim that it's easier to derive than to prove is just mathematically false It's not even false it's incoherent. But I didn't make that claim. Both derivation and verification are ways to prove a program satisfies a specification. As you say, a derivation of a program that satisfies a specification is a proof. Specifically, a proof by construction. The claim is that it's considerably easier to derive a program that satisfies some property than it is to verify if an arbitrary program satisfies that property. For example say we have a specification S: "returns a product of two primes" and two programs. P1: "Return 2^82589933-1 * 2^77232917-1" and P2: "Return 2^8258993365541237147-1". The proof of the correctness of P1 is trivial because I constructed it to be so[1]. As for P2 I have no idea if it satisfies S, but I am certain that it'll be considerably harder to convince myself and others that it does than it was for P1. > With regards to claims about informal "proofs" or "derivations" it's hard to say anything, because the problem is not well-stated. I've made no claims of the sort. [1] https://primes.utm.edu/largest.html https://primes.utm.edu/largest.html
- pron 6y ago
  > And correctly implementing those algorithms is much easier using a formal derivation 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. > You can't possibly be claiming that no formal mathematics was done before the invention of automated checkers, because that would be both ridiculous and observably false. Formal mathematics is not necessarily checked by a computer, but it is necessarily checkable by a computer. > I disagree. A specification maps to either an empty or countably infinite set of programs that satisfy it. It's not a matter of disagreement. This is the proof. A program is a specification, but it is not necessarily the only implementation of this specification. There are mathematical definitions of what it means to implement a specification (it's called the abstraction-refinement relation, and one definition is that of "simulation": https://en.wikipedia.org/wiki/Simulation_preorder https://en.wikipedia.org/wiki/Simulation_preorder). The issue of the hardness of program analysis and synthesis is not a matter of opinions, but has been studied quite extensively for decades. You can read papers on the subject by people like Philippe Schnoebelen, Rajeev Alur and quite a few others. I can't give an introduction to the subject here. > I'm better off not using mathematical reasoning to derive the programs that I do know how to write. 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. Formal methods tries to help us specify some properties and then write programs that satisfy them, even if -- and especially -- if doing so is hard or even uncertain to be possible. I'm not yet clear on what it is that you do, but I am explaining what formal program synthesis/refinement means in the context of formal methods, and what it is that hasn't been achieved. For example, taking the distributed system specification and deriving a program that implements something like Paxos. We know that easy things are easy. Formal methods are mostly for the cases that are particularly tricky. > The claim is that it's considerably easier to derive a program that satisfies some property than it is to verify if an arbitrary program satisfies that property. 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.
  - 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.

by pron 6y ago

User23 6y ago

> finding an algorithm that does it (perhaps together with some other latency requirements) is extremely hard and it took many years to find the first one that could do it. I agree. And correctly implementing those algorithms is much easier using a formal derivation with a mathematical tool such as the predicate calculus than it is by just eyeballing it and hoping your tests catch all errors. > But hard problems come up all the time, especially when concurrency is involved Predicate transformers are well suited for reasoning about nondeterminism and concurrency. > Not if it's done formally Program derivation with predicate transformers is done formally. It's a chain of equivalences, implications, and consequences as appropriate to the problem. The program text is literally developed as a proof, and each transformation of the code must be justified by axiom, theorem, or lemma and at the end of that derivation all properties of the specification hold. You can't possibly be claiming that no formal mathematics was done before the invention of automated checkers, because that would be both ridiculous and observably false. > Here is the proof: X is a program, and so, also a specification, I disagree. A specification maps to either an empty or countably infinite set of programs that satisfy it. Also all programs satisfy countably infinitely many specifications. They are not isomorphic or even dual. In this case that conflation doesn't seem to impair our understanding too much though. > and P(X) is some property that you want to verify for X. Right, and the task of the programmer is to write a program text that provably establishes that P(X) holds everywhere in the program state space. > A formal derivation of a program from the specification X ∧ P(X) will, therefore, prove P(X) Yes this is what I meant when I said you should use the same techniques to derive the program text that you would to derive any other mathematical proof. > it's not a trick, but a basic result in the study of the hardness of program analysis It's a trick because it's a clever way of saying write a program for which there is no known algorithm. As of now nobody is going to be able to do that regardless of their methodology. I get the impression that you mean this to be a compelling point, but I'm not grasping how I'm better off not using mathematical reasoning to derive the programs that I do know how to write. > The claim that it's easier to derive than to prove is just mathematically false It's not even false it's incoherent. But I didn't make that claim. Both derivation and verification are ways to prove a program satisfies a specification. As you say, a derivation of a program that satisfies a specification is a proof. Specifically, a proof by construction. The claim is that it's considerably easier to derive a program that satisfies some property than it is to verify if an arbitrary program satisfies that property. For example say we have a specification S: "returns a product of two primes" and two programs. P1: "Return 2^82589933-1 * 2^77232917-1" and P2: "Return 2^8258993365541237147-1". The proof of the correctness of P1 is trivial because I constructed it to be so[1]. As for P2 I have no idea if it satisfies S, but I am certain that it'll be considerably harder to convince myself and others that it does than it was for P1. > With regards to claims about informal "proofs" or "derivations" it's hard to say anything, because the problem is not well-stated. I've made no claims of the sort. [1] https://primes.utm.edu/largest.html https://primes.utm.edu/largest.html

pron 6y ago
> And correctly implementing those algorithms is much easier using a formal derivation 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. > You can't possibly be claiming that no formal mathematics was done before the invention of automated checkers, because that would be both ridiculous and observably false. Formal mathematics is not necessarily checked by a computer, but it is necessarily checkable by a computer. > I disagree. A specification maps to either an empty or countably infinite set of programs that satisfy it. It's not a matter of disagreement. This is the proof. A program is a specification, but it is not necessarily the only implementation of this specification. There are mathematical definitions of what it means to implement a specification (it's called the abstraction-refinement relation, and one definition is that of "simulation": https://en.wikipedia.org/wiki/Simulation_preorder https://en.wikipedia.org/wiki/Simulation_preorder). The issue of the hardness of program analysis and synthesis is not a matter of opinions, but has been studied quite extensively for decades. You can read papers on the subject by people like Philippe Schnoebelen, Rajeev Alur and quite a few others. I can't give an introduction to the subject here. > I'm better off not using mathematical reasoning to derive the programs that I do know how to write. 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. Formal methods tries to help us specify some properties and then write programs that satisfy them, even if -- and especially -- if doing so is hard or even uncertain to be possible. I'm not yet clear on what it is that you do, but I am explaining what formal program synthesis/refinement means in the context of formal methods, and what it is that hasn't been achieved. For example, taking the distributed system specification and deriving a program that implements something like Paxos. We know that easy things are easy. Formal methods are mostly for the cases that are particularly tricky. > The claim is that it's considerably easier to derive a program that satisfies some property than it is to verify if an arbitrary program satisfies that property. 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.
- 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.