4 ms·

And my point is that discussion of hypothetical ability is not what I am talking about. I can show you why there are good reasons to doubt the programmer's abil

by pron 6y ago

And my point is that discussion of hypothetical ability is not what I am talking about. I can show you why there are good reasons to doubt the programmer's ability to reason about a large program in light of computational complexity results accumulated in the last twenty years (and you are simply wrong about the bearings of model checking to the situation), but instead of trying to argue over hypotheticals, I'm merely pointing out that the ability you believe exists has never, to the best of my knowledge, actually been realised in a scalable, repeatable, affordable way in the field. If you claim you could achieve it, please try. > And I have been for over a decade. What exactly have you done for over a decade? I am quite familiar with predicate transformers, but the distance between using Hoare logic and the like on code units -- which is relatively easy and pretty widely done (e.g. with SPARK) -- and formally (which means mechanically checkable, even if it is human directed) deriving a large program from a specification is gargantuan. Proving/deriving code units from contracts and the like is not the problem I'm talking about. Neither Dijkstra nor anyone else has come remotely close to achieving it, and achieving it is a guaranteed Turing award.

User23 6y ago
> I can show you why there are good reasons to doubt the programmer's ability to reason about a large program in light of computational complexity results accumulated in the last twenty years (and you are simply wrong about the bearings of model checking to the situation) OK. Show me. This is why it's important to write the specification with an eye toward keeping the implementation manageable. This is probably a drawback of using a tool like TLA+ to check a specification. The tool makes it relatively easy to write a terribly structured specification, check it with TLA+ and declare victory, and leave the programmer in a hopeless situation. A well designed specification will unsurprisingly mirror well designed code[1]. What I have empirically tested is that keeping my functions/methods simple enough to be easily specified also keeps them easy to formally derive correct program text for. The problem of composition is treated entirely separately. You don't need to understand the fully concatenated predicate transformers for each function/method, you just need to know what wp (or another appropriate predicate transformer) is for each and be sure to satisfy it. > What exactly have you done for over a decade? Please understand this is a greatly abridged response. My general habit is to look at the requirements and infer the implied specification since a formal specification is sadly almost always missing. Thankfully most business code is theoretically trivial so postulating a reasonable specification from the requirements is easy. So, I then document my assumptions about what I believe the customer is actually asking for formally. Before I write code I think about the postcondition that I want that code to establish and determine what preconditions, if any, must hold. I put this as comments in the test modules. Then I do a more or less standard TDD approach, with the tests trivially derived from the specification[2], because management likes tests and they're paying the bills. Then I derive the code to make the tests pass from the specification using predicate transformers from the precondition to the desired postcondition. And then I run the tests and move on to the next properly isolated concern. Obviously no human discipline is infallible and I still make mistakes, but I make far fewer mistakes than I would using the typical sloppy approach most programmers use. One time I got chewed out by my manager for allowing one bug to make it into production in nine months, because I had raised expectations of the quality of my code so high. And by the way I've always just presented my methodology as TDD because of the mathematical phobia that's so prevalent in American industry. If I tell management that this code is easy to maintain, you just need programmers proficient in the predicate calculus they will dismiss me. If on the other hand I say look I have well over 90% branch coverage I'll get an attaboy and management will be happy. By this time I hope it's clear that my thoughts on the subject were not formed in the lab, but at a Big Tech Company You've Definitely Heard Of. I hope we can agree that the general tendency in industry to ignore or even deride what computing science can teach us is unfortunate. > formally (which means mechanically checkable, even if it is human directed) Dubious[3]. A mathematical formalism does not require algorithmic automated checking to exist. And even if said checking is decidable, which it mostly isn't, it may not run in a practical time on any possible mechanical computer we can conceivably build. However if you mean like any other formal mathematics where "the symbols do the work" so long as you follow the appropriate rules of derivation then I am in complete agreement. [1] Proper separation of concerns and such. [2] Obviously no tests are going to exhaustively check a non-trivial specification, but my approach is still strictly better than the typical practice of primarily optimizing for satisfying coverage tools. [3] https://en.wikipedia.org/wiki/Formalism_(philosophy_of_mathematics) https://en.wikipedia.org/wiki/Formalism_(philosophy_of_mathe...
- pron 6y ago
  > OK. Show me. Here is a simple specification: write a program that, given a positive even integer, returns two prime integers, whose some is the input, and never fails to do so. Start with a formal statement of the requirement, and derive a program that provably satisfies it. Decompose your program however you like. > Then I derive the code to make the tests pass from the specification Do you use predicate transformers all the way from a high-level spec to each and every line in a 1MLOC distributed and interactive system, with management consoles, reports and ten-thousand users per server? > A mathematical formalism does not require algorithmic automated checking to exist. It most certainly does. That is the literal meaning of "formal" in formal logic/method/synthesis/verification. A formal logic has a proof theory made of inference rules. It means that conclusions are reached by manipulation of the syntactic form -- hence formal -- without use of any mathematical intuition. Alan Turing then showed that a proof system can always be described as a Turing machine, and that formal = mechanical. There is a huge gap between informal mathematical reasoning and formal reasoning. I believe I've seen someone mention an exponential blowup in proof size of formal proofs compared to mathematical proofs. > Obviously no human discipline is infallible and I still make mistakes, but I make far fewer mistakes than I would using the typical sloppy approach most programmers use. There's a very, very wide gap between "disciplined" and formal. I am all for disciplined and for using formal methods in various places. End-to-end formal derivation/verification, i.e. from high-level spec to code, in a scalable, feasible manner, is yet to be achieved.
  - User23 6y ago
    > Here is a simple specification: write a program that, given a positive even integer, returns two prime integers, whose some is the input, and never fails to do so. I'm not going to solve Goldbach's conjecture on hackernews or anywhere else. I wish I could, I really do, but my incapability there doesn't invalidate my arguments. I'm not even annoyed though, that was a cute trick and I appreciate your cleverness. Fortunately Fields Medal tier mathematical problems have never come up in my professional programming career. > It most certainly does. That is the literal meaning of "formal" in formal logic/method/synthesis/verification. A formal logic has a proof theory made of inference rules. It means that conclusions are reached by manipulation of the syntactic form -- hence formal -- without use of any mathematical intuition. Once again, I completely agree with this. Let the symbols do the work. But we keep coming back to the same misunderstanding. A program can feasibly be derived that can't feasibly be verified without access to the discrete documented steps of the derivation[1]. Showing the work of the derivation is sufficient to convince any honest interlocutor of the correctness of the proof. It may well be enough to allow an algorithm to perform the verification too, I'll defer to your expertise on that. In any event, as I said before using the analogy of primes, verification is rather a lot harder than construction. Edit: Also I want you to know I'm finding this a pleasant discussion and am thankful that you're taking the time to help develop my thoughts and hopefully yours too. [1] By analogy, factoring the product of two primes is easy when in addition to being given the product you are also given the multiplier and multiplicand.

by pron 6y ago

User23 6y ago

> I can show you why there are good reasons to doubt the programmer's ability to reason about a large program in light of computational complexity results accumulated in the last twenty years (and you are simply wrong about the bearings of model checking to the situation) OK. Show me. This is why it's important to write the specification with an eye toward keeping the implementation manageable. This is probably a drawback of using a tool like TLA+ to check a specification. The tool makes it relatively easy to write a terribly structured specification, check it with TLA+ and declare victory, and leave the programmer in a hopeless situation. A well designed specification will unsurprisingly mirror well designed code[1]. What I have empirically tested is that keeping my functions/methods simple enough to be easily specified also keeps them easy to formally derive correct program text for. The problem of composition is treated entirely separately. You don't need to understand the fully concatenated predicate transformers for each function/method, you just need to know what wp (or another appropriate predicate transformer) is for each and be sure to satisfy it. > What exactly have you done for over a decade? Please understand this is a greatly abridged response. My general habit is to look at the requirements and infer the implied specification since a formal specification is sadly almost always missing. Thankfully most business code is theoretically trivial so postulating a reasonable specification from the requirements is easy. So, I then document my assumptions about what I believe the customer is actually asking for formally. Before I write code I think about the postcondition that I want that code to establish and determine what preconditions, if any, must hold. I put this as comments in the test modules. Then I do a more or less standard TDD approach, with the tests trivially derived from the specification[2], because management likes tests and they're paying the bills. Then I derive the code to make the tests pass from the specification using predicate transformers from the precondition to the desired postcondition. And then I run the tests and move on to the next properly isolated concern. Obviously no human discipline is infallible and I still make mistakes, but I make far fewer mistakes than I would using the typical sloppy approach most programmers use. One time I got chewed out by my manager for allowing one bug to make it into production in nine months, because I had raised expectations of the quality of my code so high. And by the way I've always just presented my methodology as TDD because of the mathematical phobia that's so prevalent in American industry. If I tell management that this code is easy to maintain, you just need programmers proficient in the predicate calculus they will dismiss me. If on the other hand I say look I have well over 90% branch coverage I'll get an attaboy and management will be happy. By this time I hope it's clear that my thoughts on the subject were not formed in the lab, but at a Big Tech Company You've Definitely Heard Of. I hope we can agree that the general tendency in industry to ignore or even deride what computing science can teach us is unfortunate. > formally (which means mechanically checkable, even if it is human directed) Dubious[3]. A mathematical formalism does not require algorithmic automated checking to exist. And even if said checking is decidable, which it mostly isn't, it may not run in a practical time on any possible mechanical computer we can conceivably build. However if you mean like any other formal mathematics where "the symbols do the work" so long as you follow the appropriate rules of derivation then I am in complete agreement. [1] Proper separation of concerns and such. [2] Obviously no tests are going to exhaustively check a non-trivial specification, but my approach is still strictly better than the typical practice of primarily optimizing for satisfying coverage tools. [3] https://en.wikipedia.org/wiki/Formalism_(philosophy_of_mathematics) https://en.wikipedia.org/wiki/Formalism_(philosophy_of_mathe...

pron 6y ago
> OK. Show me. Here is a simple specification: write a program that, given a positive even integer, returns two prime integers, whose some is the input, and never fails to do so. Start with a formal statement of the requirement, and derive a program that provably satisfies it. Decompose your program however you like. > Then I derive the code to make the tests pass from the specification Do you use predicate transformers all the way from a high-level spec to each and every line in a 1MLOC distributed and interactive system, with management consoles, reports and ten-thousand users per server? > A mathematical formalism does not require algorithmic automated checking to exist. It most certainly does. That is the literal meaning of "formal" in formal logic/method/synthesis/verification. A formal logic has a proof theory made of inference rules. It means that conclusions are reached by manipulation of the syntactic form -- hence formal -- without use of any mathematical intuition. Alan Turing then showed that a proof system can always be described as a Turing machine, and that formal = mechanical. There is a huge gap between informal mathematical reasoning and formal reasoning. I believe I've seen someone mention an exponential blowup in proof size of formal proofs compared to mathematical proofs. > Obviously no human discipline is infallible and I still make mistakes, but I make far fewer mistakes than I would using the typical sloppy approach most programmers use. There's a very, very wide gap between "disciplined" and formal. I am all for disciplined and for using formal methods in various places. End-to-end formal derivation/verification, i.e. from high-level spec to code, in a scalable, feasible manner, is yet to be achieved.
- User23 6y ago
  > Here is a simple specification: write a program that, given a positive even integer, returns two prime integers, whose some is the input, and never fails to do so. I'm not going to solve Goldbach's conjecture on hackernews or anywhere else. I wish I could, I really do, but my incapability there doesn't invalidate my arguments. I'm not even annoyed though, that was a cute trick and I appreciate your cleverness. Fortunately Fields Medal tier mathematical problems have never come up in my professional programming career. > It most certainly does. That is the literal meaning of "formal" in formal logic/method/synthesis/verification. A formal logic has a proof theory made of inference rules. It means that conclusions are reached by manipulation of the syntactic form -- hence formal -- without use of any mathematical intuition. Once again, I completely agree with this. Let the symbols do the work. But we keep coming back to the same misunderstanding. A program can feasibly be derived that can't feasibly be verified without access to the discrete documented steps of the derivation[1]. Showing the work of the derivation is sufficient to convince any honest interlocutor of the correctness of the proof. It may well be enough to allow an algorithm to perform the verification too, I'll defer to your expertise on that. In any event, as I said before using the analogy of primes, verification is rather a lot harder than construction. Edit: Also I want you to know I'm finding this a pleasant discussion and am thankful that you're taking the time to help develop my thoughts and hopefully yours too. [1] By analogy, factoring the product of two primes is easy when in addition to being given the product you are also given the multiplier and multiplicand.