4 ms·

There is one advantage of formal specs in general that static types inherent: they can enforce a correctness policy on a design that works for all inputs with n

There is one advantage of formal specs in general that static types inherent: they can enforce a correctness policy on a design that works for all inputs with no runtime overhead. SPARK Ada eliminating entire classes of errors with mostly-automated analysis is one example. Rust blocking temporal and some concurrency errors without GC is another. I'll note they're both hard to eliminate with testing, too. With that, comes the next benefit: less debugging and lower maintenance costs. It has to be balanced against annotation costs. Most projects claimed to come out ahead if it was just safety rather than full correctness. You can also generate tests and runtime checks from specs to get those benefits. So, for high reliability with lower maintenance, there's definitely an advantage to knocking out entire classes of error. That leads to last advantage Ill mention: ability to warranty (market) and certify (regulators) your code free of those defects [if the checker worked]. The checkers are also tiny on some systems. Rarely fail. Inspires extra confidence.

sifoobar 8y ago
Sure, in return for bending code over backwards to fit rules you get guarantees; but pretending that is anything but a different compromise isn't helping. If Ada was all that, everyone would be using it; and that's not going to happen, because it's not a realistic approach to programming. The academic approach doesn't look very constructive to me, never did. Once you have a language nailed down so hard that errors aren't possible, the complexity of dealing with it will be more or less the same as dealing with the errors in the first place. I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety.
- nickpsecurity 8y ago
  "If Ada was all that, everyone would be using it" Argument for popularity = superiority. By your same logic, we shouldve stuck with COBOL for important apps since all the big businesses were using it. I have a feeling you dont write new apps in COBOL. "the complexity of dealing with it will be more or less the same as dealing with the errors in the first place." The best empirical comparison of C and Ada showed the opposite. All studies showed the safer languages had less defects with usually more productivity due to less rework later on. Evidence is against your claim so far. "I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety." Me too. Rust and Nim are taking that approach. People are finding both useful in production so far.

sifoobar 8y ago

Sure, in return for bending code over backwards to fit rules you get guarantees; but pretending that is anything but a different compromise isn't helping. If Ada was all that, everyone would be using it; and that's not going to happen, because it's not a realistic approach to programming. The academic approach doesn't look very constructive to me, never did. Once you have a language nailed down so hard that errors aren't possible, the complexity of dealing with it will be more or less the same as dealing with the errors in the first place. I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety.

nickpsecurity 8y ago
"If Ada was all that, everyone would be using it" Argument for popularity = superiority. By your same logic, we shouldve stuck with COBOL for important apps since all the big businesses were using it. I have a feeling you dont write new apps in COBOL. "the complexity of dealing with it will be more or less the same as dealing with the errors in the first place." The best empirical comparison of C and Ada showed the opposite. All studies showed the safer languages had less defects with usually more productivity due to less rework later on. Evidence is against your claim so far. "I would much prefer a focus on more powerful tools that fit into the current "unsafe" ecosystem while offering a more gradual and flexible path to improved safety." Me too. Rust and Nim are taking that approach. People are finding both useful in production so far.