I believe already some 2 decades ago Bill Gates said that the biggest failure in software is the lack of productivity gains in software development.

Just to cherry pick a dramatized example. In the late 90s, one of my first programming experiences was in Delphi. It's a very visual way to program. You drag and drop a UI together from standardized elements. You could data bind things like input fields to a data source. You'd double click a button and it takes you to the already created "onclick" event where you do the actual coding. In a way, this is still similar to how you can "program" Microsoft Access today.

In this same period (I was in a computer science study) I was moaning to my teacher how tricky programming in C was. I made tiny memory management errors crashing the entire PC, with zero debug output.

His words: "Don't worry. By the time you get to work, you'll just do modeling".

Now I work on the web. It's been 30 years since Delphi and instead of productivity gains, we've taken steps in the opposite direction. There is no standardized UI library. JavaScript has no standard library. There's no single unified architecture. There's no standard tool chain. It's all very low level after which we stitch together fragile semi-abstractions.

I know it's an imperfect comparison, but I hope it gets the point across. It's all far too low level and fragile.

This doesn't just hurt productivity, also accessibility. It's simply not beginner friendly.

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.

> 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

[2] https://github.com/dafny-lang/dafny