5 ms·

You don’t even need to do a study to arrive at this conclusion. Has no one read Djikstra’s writings? https://www.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF http

You don’t even need to do a study to arrive at this conclusion. Has no one read Djikstra’s writings? https://www.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF https://www.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF “Program testing can be used to show the presence of bugs, but never to show their absence!” Everybody in our industry wants to bash math and say that anyone can write programs, but programs are logical systems and can only be fully understood with math and logic. We have the tools for understanding and reasoning about infinitely large structures, programmers just refuse to use them, and even deride them. Well, I am not in that camp, and I work on math and logic skills to help me develop working software. It isn’t perfect, but it’s the only path that makes sense to me. > But complexity sells better and the market pulls in the opposite direction. I still remember finding a book on how to use "Wordperfect 5.0" of more than 850 pages, in fact a dozen pages more than my 1951 edition of Georg Joos, "Theoretical Physics"! It is time to unmask the computing community as a Secret Society for the Creation and Preservation of Artificial Complexity. And then we have the software engineers, who only mention formal methods in order to throw suspicion on them. In short, we should not expect too much support from the computing community at large. And from the mathematical community I have learned not to expect too much support either, as informality is the hallmark of the Mathematical Guild, whose members —like poor programmers— derive their intellectual excitement from not quite knowing what they are doing and prefer to be thrilled by the marvel of the human mind (in particular their own ones). For them, the Dream of Leibniz is a Nightmare. In summary, we are on our own. But that does not matter. In the next fifty years, Mathematics will emerge as The Art and Science of Effective Formal Reasoning, and we shall derive our intellectual excitement from learning How to Let the Symbols Do the Work. Calculemus! https://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/EWD1243a.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD12xx/E...

brabel 5y ago
> We have the tools for understanding and reasoning about infinitely large structures, programmers just refuse to use them, and even deride them. Could you point out which tools you're talking about?
- amw-zero 5y ago
  Well, by this I mean math (and mathematical logic). Math is the tool for reasoning about possibly infinite concepts, i.e. you can make a statement about infinite sets and still know if it’s true or not. We aren’t limited to what we can see and touch, which is good because any non-trivial software application is so large that it could never be drawn out like a building blueprint. It can only be described and reasoned about abstractly. But, you are probably asking about what ‘tools’ can be applied to programming, meaning some kind of library or application. These are also out there. Here’s a few that I think are promising: TLA+: This is a specification language for describing and reasoning about computations as state machines, with a particular focus on modeling distributed systems. It has been used at Amazon to check designs for their distributed algorithms. They have used it to check parts of S3 for example: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... Best reference is the book Specifying Systems: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf https://lamport.azurewebsites.net/tla/book-02-08-08.pdf. Then you have theorem provers / proof assistants based on type theory. These are frankly complex, but getting better. F*: This one is the most exciting to me. It’s currently being used to develop a formally verified HTTPS stack: https://project-everest.github.io/ https://project-everest.github.io/. They already have components released to the Linux kernel and Firefox. One of the most exciting things about this tool is that you can verify an efficient, stateful algorithm and extract highly performant C code from it. Their verified implementations have equal or better performance to the current solutions out there. So all of the overhead is for verification, none exists at runtime. Of course you can’t talk about proof assistants without mentioning Coq. Its claim to fame is producing a formally verified C compiler, CompCert: https://compcert.org/ https://compcert.org/. As you can see, so far, formal verification has been mostly limited to components of systems, not entire systems. But, it’s a start, and the scope of what we can verify is getting larger.
  - brabel 5y ago
    I know about all the tools you've mentioned as I've been following the space from a distance, was just curious if you had a more "outside research" approach in mind when you claimed developers refuse to use the available "tools"... I haven't seen Coq, or even Idris or Ada+Spark, which arguably much closer-to-the-industry tools, being used for anything but very niche cases (like the case you mentioned about using TLA+ at Amazon). I am probably one of the developers who would gladly use anything like that, but from my brief experiments and knowledge, they are very, very far from becoming usable in a general setting, so no, I don't refuse to use the tools, the tools are just not good enough to justify the high cost of using them yet.

brabel 5y ago

> We have the tools for understanding and reasoning about infinitely large structures, programmers just refuse to use them, and even deride them. Could you point out which tools you're talking about?

amw-zero 5y ago
Well, by this I mean math (and mathematical logic). Math is the tool for reasoning about possibly infinite concepts, i.e. you can make a statement about infinite sets and still know if it’s true or not. We aren’t limited to what we can see and touch, which is good because any non-trivial software application is so large that it could never be drawn out like a building blueprint. It can only be described and reasoned about abstractly. But, you are probably asking about what ‘tools’ can be applied to programming, meaning some kind of library or application. These are also out there. Here’s a few that I think are promising: TLA+: This is a specification language for describing and reasoning about computations as state machines, with a particular focus on modeling distributed systems. It has been used at Amazon to check designs for their distributed algorithms. They have used it to check parts of S3 for example: https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon.... Best reference is the book Specifying Systems: https://lamport.azurewebsites.net/tla/book-02-08-08.pdf https://lamport.azurewebsites.net/tla/book-02-08-08.pdf. Then you have theorem provers / proof assistants based on type theory. These are frankly complex, but getting better. F*: This one is the most exciting to me. It’s currently being used to develop a formally verified HTTPS stack: https://project-everest.github.io/ https://project-everest.github.io/. They already have components released to the Linux kernel and Firefox. One of the most exciting things about this tool is that you can verify an efficient, stateful algorithm and extract highly performant C code from it. Their verified implementations have equal or better performance to the current solutions out there. So all of the overhead is for verification, none exists at runtime. Of course you can’t talk about proof assistants without mentioning Coq. Its claim to fame is producing a formally verified C compiler, CompCert: https://compcert.org/ https://compcert.org/. As you can see, so far, formal verification has been mostly limited to components of systems, not entire systems. But, it’s a start, and the scope of what we can verify is getting larger.
- brabel 5y ago
  I know about all the tools you've mentioned as I've been following the space from a distance, was just curious if you had a more "outside research" approach in mind when you claimed developers refuse to use the available "tools"... I haven't seen Coq, or even Idris or Ada+Spark, which arguably much closer-to-the-industry tools, being used for anything but very niche cases (like the case you mentioned about using TLA+ at Amazon). I am probably one of the developers who would gladly use anything like that, but from my brief experiments and knowledge, they are very, very far from becoming usable in a general setting, so no, I don't refuse to use the tools, the tools are just not good enough to justify the high cost of using them yet.