3 ms·

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 infinit

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.
- amw-zero 5y ago
  It boils down to two camps: open to formal methods, and not open to formal methods. And, I would say the overwhelming majority of developers, especially here on HN, are in the "not open to formal methods" camp. I can find comments that justify that, there are also data points from speaking with coworkers and colleagues. So that is what I was talking about when saying that logs of people "refuse the tools." They just aren't even open to them to begin with. You sound open to them, but dissatisfied with the tools themselves. I'm honestly in that camp too! We are not there yet in terms of being able to use this as the primary way that an entire application is developed. But, I believe that's the direction we should go in. You're right - we really need a tool that wins people over with the cost to value ratio. The promise of something far off in the future isn't enough for most people.

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.

amw-zero 5y ago
It boils down to two camps: open to formal methods, and not open to formal methods. And, I would say the overwhelming majority of developers, especially here on HN, are in the "not open to formal methods" camp. I can find comments that justify that, there are also data points from speaking with coworkers and colleagues. So that is what I was talking about when saying that logs of people "refuse the tools." They just aren't even open to them to begin with. You sound open to them, but dissatisfied with the tools themselves. I'm honestly in that camp too! We are not there yet in terms of being able to use this as the primary way that an entire application is developed. But, I believe that's the direction we should go in. You're right - we really need a tool that wins people over with the cost to value ratio. The promise of something far off in the future isn't enough for most people.