4 ms·

This is similar to the conclusion I came to after doing my PhD in a CS department that had lots of people enamored by formal methods: that the usefulness of it

This is similar to the conclusion I came to after doing my PhD in a CS department that had lots of people enamored by formal methods: that the usefulness of it is inversely proportional to the complexity of the project to be verified. Sad that apparently hasn't changed much in the 20 years since. I say "enamored", because formal methods seems to me like a field that gets a lot of attention because the possible outcome of it is so damn attractive: if we indeed could easily prove software correct, that would be the biggest advance in software, EVER. But is a bit of a fallacy that just because the imagined end result is so elegant and desirable, that there must be a path to it. Also, any gains that can be claimed by formal methods are hard to evaluate in a vacuum, as using any other techniques that involve spending 10x more time thinking about / working with some code can possibly have equally beneficial reductions in bug counts. Most software that has undesirable bugs is such because no time/money investment is deemed worth it to make it better, not because formal methods is the only way to improve it. I find it funny that meanwhile, mainstream software is going the opposite direction, with ever larger systems written in dynamically typed languages like JavaScript and Python, or overly simplistic static type systems like those of Java and Go. You'd think if formal methods was our far away desirable future we'd be incrementally moving in that direction by using more expressive type systems (Haskell, Rust..) and maybe even dependent typing. The invariants that can be encoded in such systems can rule out usefully large classes of bugs with way lower effort than formal methods, but somehow movement on that front is slow. If so few people care to even grab the low hanging fruit, why do formal methods people think we can jump from chaos to order in one step?

toast0 9y ago
For me, the problem with formal methods is that a prerequisite is a (formal) specification, and I've never seen one of those in 20 years of software work.
- Aardappel 9y ago
  Yes. And the ones I did encounter had zero "testing" done to see if they corresponded to the real world. Hence why we need more incremental tools, that allow us to encode more rules into the (type) systems we already use.
  - catnaroek 9y ago
    > And the ones I did encounter had zero "testing" done to see if they corresponded to the real world. You can excuse human beings for being unable to write the programs they want, but if they can't even specify the programs they want, they don't deserve the epithet Homo sapiens.
- tom_mellior 9y ago
  That depends on what you want to use formal methods for. For full functional correctness, yes, you need a spec. But much can be gained by just proving the absence of runtime errors, i.e., for C, things like "all array accesses are in bounds", "every dereferenced pointer is valid", or "integer arithmetic never overflows". Formal methods tools for C have those baked in, so you can get going quickly without specifying these things yourself. It's still hard, though.

toast0 9y ago

For me, the problem with formal methods is that a prerequisite is a (formal) specification, and I've never seen one of those in 20 years of software work.

Aardappel 9y ago
Yes. And the ones I did encounter had zero "testing" done to see if they corresponded to the real world. Hence why we need more incremental tools, that allow us to encode more rules into the (type) systems we already use.
- catnaroek 9y ago
  > And the ones I did encounter had zero "testing" done to see if they corresponded to the real world. You can excuse human beings for being unable to write the programs they want, but if they can't even specify the programs they want, they don't deserve the epithet Homo sapiens.
tom_mellior 9y ago
That depends on what you want to use formal methods for. For full functional correctness, yes, you need a spec. But much can be gained by just proving the absence of runtime errors, i.e., for C, things like "all array accesses are in bounds", "every dereferenced pointer is valid", or "integer arithmetic never overflows". Formal methods tools for C have those baked in, so you can get going quickly without specifying these things yourself. It's still hard, though.