4 ms·

> just using mathematical reasoning as you derive your program text makes it considerably easier to build systems that satisfy the specification. And I am sayi

by pron 6y ago

> just using mathematical reasoning as you derive your program text makes it considerably easier to build systems that satisfy the specification. And I am saying that since this has never been achieved in practice for systems of considerable scale, this is a rather hypothetical use of the word "easier." Is it possible that one day this will actually be easier? Sure. Is this the case now? I don't think so. > The human act of writing the program is exactly the same as deriving a proof. The human act of painting your ceiling is exactly the same as painting the Sistine Chapel and the human act done by a first-year student taking a calculus exam is exactly the same as a Field medalist writing a proof in a paper. Look at how, say, a verified quicksort is written in Idris [1] and compare that to how it's written in Java/Python (one could write Quicksort in Idris as in Java, but then the program will not serve as proof of its correctness). I think that the claim that with what we know how to do today producing the former is as easy as the latter, let alone easier, requires some empirical evidence. [1]: https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris https://github.com/bmsherman/blog/wiki/Quicksort-in-Idris

User23 6y ago
> And I am saying that since this has never been achieved in practice for systems of considerable scale, this is a rather hypothetical use of the word "easier." Is it possible that one day this will actually be easier? Sure. Is this the case now? I don't think so. Respectfully, I recommend that you read Dijkstra's A Discipline of Programming that I linked above. I think you'll find it interesting at the very least and possibly even enlightening. I assume you are a product of the American educational system, where these concepts are rarely taught. There are exceptions though, for example the great Leslie Lamport has also done notable work[1] in this area. You'll find that out of necessity on some level we all have to reason about state spaces and the possible coordinates in those spaces to write software. Using formal mathematical reasoning is strictly better than the sloppy approach generally used. I'm not claiming that it's a magic bullet though. Even mathematicians make errors after all. There are various middle grounds too. Done properly, TDD and its cousins amount to an implied specification and "ensure" that the program written will satisfy the tested subset of said implied specification. The primary practical limitation of this approach is that testing can never show the absence of errors, only their presence. > The human act of painting your ceiling is exactly the same as painting the Sistine Chapel and the human act done by a first-year student taking a calculus exam is exactly the same as a Field medalist writing a proof in a paper. You've lost me here, I don't at all understand how these analogies have anything to do with the kind of reasoning a human can do about programs vs the kind of "reasoning" programs can do about programs. The point is that it doesn't matter what language a program is written in. The program text is always a mathematical object describing a state space (usually reasoned about as a set of state spaces like structs or objects) and transformations in those state spaces. Granted, some languages, like Perl, have ill-defined semantics that make reasoning about correctness impracticable, but often it's possible to restrict oneself to a subset of the language that can be reasoned about. For what it's worth I've applied these techniques quite successfully in my professional life. I hate getting paged and I hate debugging, so I've found it useful to learn to write correct software. I seriously doubt that I'm the only one, but as I've said before there is some kind of bizarre phobia American programmers have about being told that what they are doing is math that makes it very hard to talk about with most of them. [1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf https://lamport.azurewebsites.net/pubs/lamport-win.pdf
- pron 6y ago
  I think you are not sufficiently familiar with this field, Dijkstra wrote "Discipline" years before computational complexity results on program analysis were known, and I think you misunderstand the tremendous gap between what works on small examples in the lab and what is scalable enough to be applied widely in the field and the difference between something that might be possible in principle vs. something that's affordably feasible in practice. We know more than Dijkstra did, the techniques have improved, and still no "ordinary" (non-niche) real-world software of any significant size has been written using formal refinement to date. If you claim this is possible today -- go ahead and do it for a medium-sized program of say, at least 100KLOC. A formalism like TLA+ is well suited for this task, so go ahead and try. I am not American, I don't like making generalisations about Americans or any other nationality, and, as you could see from my blog, I am very much in favour of employing maths in system design -- that's what TLA+ is all about. But confusing "mathematical object" with "can be feasibly reasoned about" is just ignoring computational complexity. I can give you an example of two subroutines, each only a few lines long and each very simple to understand, and yet you won't be able to answer a most basic question about their composition. Complexity theory tells us that mathematical problems have an inherent hardness, and the fact you can write them does not mean you can feasibly solve them. There are no simple answers here. In some carefully constructed ways formal methods can help in some specific circumstances, different methods helping in different use-cases, and you cannot just say that it's "better" overall. For example, while programs of millions of lines of code are routinely tested, no one has ever managed to formally reason about deep properties of programs of this size.
  - User23 6y ago
    I take it that means you've never read Discipline or Predicate Calculus and Program Semantics. I don't doubt your expertise in TLA+, as I hope you can see from my studious agreement with you on the items that are clearly within your expertise, but on this point you're not even wrong. You are attempting to refute the claim that a human programmer can derive a program that has desired properties more effectively with mathematical reasoning than without it by offering the objection that mechanical verification has high computational complexity[1]. That is sheer nonsense. It's like saying that because factoring products of primes is hard that it's in no way feasible to multiply them rigorously so just use an estimate instead. As an aside, the avionics for the Space Shuttle was over 250KLOC and was proved correct from the bottom up. And it functioned flawlessly. This was done before computational complexity results on program analysis were known, but that lack of knowledge was observably irrelevant to building correct software. Sadly, the hardware left a bit to be desired. [1] It's undecidable in the general case.

by pron 6y ago

User23 6y ago

> And I am saying that since this has never been achieved in practice for systems of considerable scale, this is a rather hypothetical use of the word "easier." Is it possible that one day this will actually be easier? Sure. Is this the case now? I don't think so. Respectfully, I recommend that you read Dijkstra's A Discipline of Programming that I linked above. I think you'll find it interesting at the very least and possibly even enlightening. I assume you are a product of the American educational system, where these concepts are rarely taught. There are exceptions though, for example the great Leslie Lamport has also done notable work[1] in this area. You'll find that out of necessity on some level we all have to reason about state spaces and the possible coordinates in those spaces to write software. Using formal mathematical reasoning is strictly better than the sloppy approach generally used. I'm not claiming that it's a magic bullet though. Even mathematicians make errors after all. There are various middle grounds too. Done properly, TDD and its cousins amount to an implied specification and "ensure" that the program written will satisfy the tested subset of said implied specification. The primary practical limitation of this approach is that testing can never show the absence of errors, only their presence. > The human act of painting your ceiling is exactly the same as painting the Sistine Chapel and the human act done by a first-year student taking a calculus exam is exactly the same as a Field medalist writing a proof in a paper. You've lost me here, I don't at all understand how these analogies have anything to do with the kind of reasoning a human can do about programs vs the kind of "reasoning" programs can do about programs. The point is that it doesn't matter what language a program is written in. The program text is always a mathematical object describing a state space (usually reasoned about as a set of state spaces like structs or objects) and transformations in those state spaces. Granted, some languages, like Perl, have ill-defined semantics that make reasoning about correctness impracticable, but often it's possible to restrict oneself to a subset of the language that can be reasoned about. For what it's worth I've applied these techniques quite successfully in my professional life. I hate getting paged and I hate debugging, so I've found it useful to learn to write correct software. I seriously doubt that I'm the only one, but as I've said before there is some kind of bizarre phobia American programmers have about being told that what they are doing is math that makes it very hard to talk about with most of them. [1] https://lamport.azurewebsites.net/pubs/lamport-win.pdf https://lamport.azurewebsites.net/pubs/lamport-win.pdf

pron 6y ago
I think you are not sufficiently familiar with this field, Dijkstra wrote "Discipline" years before computational complexity results on program analysis were known, and I think you misunderstand the tremendous gap between what works on small examples in the lab and what is scalable enough to be applied widely in the field and the difference between something that might be possible in principle vs. something that's affordably feasible in practice. We know more than Dijkstra did, the techniques have improved, and still no "ordinary" (non-niche) real-world software of any significant size has been written using formal refinement to date. If you claim this is possible today -- go ahead and do it for a medium-sized program of say, at least 100KLOC. A formalism like TLA+ is well suited for this task, so go ahead and try. I am not American, I don't like making generalisations about Americans or any other nationality, and, as you could see from my blog, I am very much in favour of employing maths in system design -- that's what TLA+ is all about. But confusing "mathematical object" with "can be feasibly reasoned about" is just ignoring computational complexity. I can give you an example of two subroutines, each only a few lines long and each very simple to understand, and yet you won't be able to answer a most basic question about their composition. Complexity theory tells us that mathematical problems have an inherent hardness, and the fact you can write them does not mean you can feasibly solve them. There are no simple answers here. In some carefully constructed ways formal methods can help in some specific circumstances, different methods helping in different use-cases, and you cannot just say that it's "better" overall. For example, while programs of millions of lines of code are routinely tested, no one has ever managed to formally reason about deep properties of programs of this size.
- User23 6y ago
  I take it that means you've never read Discipline or Predicate Calculus and Program Semantics. I don't doubt your expertise in TLA+, as I hope you can see from my studious agreement with you on the items that are clearly within your expertise, but on this point you're not even wrong. You are attempting to refute the claim that a human programmer can derive a program that has desired properties more effectively with mathematical reasoning than without it by offering the objection that mechanical verification has high computational complexity[1]. That is sheer nonsense. It's like saying that because factoring products of primes is hard that it's in no way feasible to multiply them rigorously so just use an estimate instead. As an aside, the avionics for the Space Shuttle was over 250KLOC and was proved correct from the bottom up. And it functioned flawlessly. This was done before computational complexity results on program analysis were known, but that lack of knowledge was observably irrelevant to building correct software. Sadly, the hardware left a bit to be desired. [1] It's undecidable in the general case.