3 ms·

At least from the systems programming perspective I think productivity gains have been significant. Valgrind had _just_ appeared as I was doing my undergrad and

At least from the systems programming perspective I think productivity gains have been significant. Valgrind had _just_ appeared as I was doing my undergrad and it allowed me to focus on the high-level math of data structures -- as an example -- compared to my non-Valgrind using classmates that were struggling with memory bugs (which, of course, I did too, but to a less degree). C++ has noticeably improved since then, if you can hew to the newer bits of the language and keep all the arcane bits in your mind. Rust has arrived on the scene, inspired by Cyclone, C++, SML and is a serious jump in productivity over C++ because the compiler keeps track of all those arcane bits. If you squint, Go's in the mix for web stuff that doesn't mind GC. It's a shame ATS didn't become more of a thing, Ada has made real strides back from the dead, especially if you can stick to SPARK Ada. We're even seeing more formal verification of complex bits of software in systems-land, something that seemed basically impossible when I first read about Coq twenty something years ago. I do admit, though, that front-end seems like a wild west presently, to my ignorant eyes.

nextos 4y ago
> Ada has made real strides back from the dead, especially if you can stick to SPARK Ada. We're even seeing more formal verification of complex bits of software in systems-land, something that seemed basically impossible when I first read about Coq twenty something years ago. I really agree with this. The situation is a bit crazy. Since formal proofs are hard, the alternative taken is giving no guarantees at all. That's bad. Static analyzers can get really far. Contracts, even just at runtime are really useful. I don't want a piece of code to run if the precondition is not met, and I don't want it to return or have side effects if the postcondition is not met. This would rule out a massive class of errors. Of course, bonus points if you can do it at compile time. Ada SPARK, Infer [1] and Dafny [2] show that rigorous engineering is possible and practical. Actually, Facebook (Meta now) argues Infer let's them move faster. I think the problem is political and economical. It's hard to monetize this first. I wish someone like Apple took the plunge and rebuilt a simpler version of their stack using formal verification. It's the kind of thing only a large corporation or a government can do because it might take half a decade to take off. Once it takes off its unstoppable. Who would not like to buy e.g. a phone where most bugs and security breaches are impossible by construction? Verification also has a nice side effect. Change for the sake of change and featuritis are pretty incompatible with it. [1] https://fbinfer.com https://fbinfer.com [2] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny
- nl 4y ago
  There's a bunch of interesting work happening in the blockchain space around formal verification languages that can compile to smart contracts. Makes sense - not only do you lose money if you get it wrong but it is very difficult to correct!
- pyjarrett 4y ago
  The great thing about Ada/SPARK is that it has a package manager now (Alire). This means there are existing SPARK packages you can use, and you can share what you make. SPARK is also an Ada subset, so you can use verified components inside your Ada programs.

nextos 4y ago

> Ada has made real strides back from the dead, especially if you can stick to SPARK Ada. We're even seeing more formal verification of complex bits of software in systems-land, something that seemed basically impossible when I first read about Coq twenty something years ago. I really agree with this. The situation is a bit crazy. Since formal proofs are hard, the alternative taken is giving no guarantees at all. That's bad. Static analyzers can get really far. Contracts, even just at runtime are really useful. I don't want a piece of code to run if the precondition is not met, and I don't want it to return or have side effects if the postcondition is not met. This would rule out a massive class of errors. Of course, bonus points if you can do it at compile time. Ada SPARK, Infer [1] and Dafny [2] show that rigorous engineering is possible and practical. Actually, Facebook (Meta now) argues Infer let's them move faster. I think the problem is political and economical. It's hard to monetize this first. I wish someone like Apple took the plunge and rebuilt a simpler version of their stack using formal verification. It's the kind of thing only a large corporation or a government can do because it might take half a decade to take off. Once it takes off its unstoppable. Who would not like to buy e.g. a phone where most bugs and security breaches are impossible by construction? Verification also has a nice side effect. Change for the sake of change and featuritis are pretty incompatible with it. [1] https://fbinfer.com https://fbinfer.com [2] https://github.com/dafny-lang/dafny https://github.com/dafny-lang/dafny

nl 4y ago
There's a bunch of interesting work happening in the blockchain space around formal verification languages that can compile to smart contracts. Makes sense - not only do you lose money if you get it wrong but it is very difficult to correct!
pyjarrett 4y ago
The great thing about Ada/SPARK is that it has a package manager now (Alire). This means there are existing SPARK packages you can use, and you can share what you make. SPARK is also an Ada subset, so you can use verified components inside your Ada programs.