Was about to suggest this myself. I see a few that didn't like this and I can see why, but I thought it was interesting to listen too. Always interesting to hear someone knowledgeable argue for something you don't think you agree with. It is also interesting since Rich is in the quite unique position of handling a functional language with dynamic types (a dying breed in the functional space imo).
I don't think Rich fully convinced me to change my mind, but he made me think about when and why Maybe is needed.
I think dynamic FP programming is actually doing quite well these days. Apart from Clojure & ClojureScript, there's Erlang and Elixir, and the Racket community, and in addition it's become popular to write FP code in Javascript using Ramda, immutable.js & etc - not to mention the FP nature of React.
Dying breed based on what? They're different compromises, there is nothing inherently superior about static types. It's more popular right now, because we're very much into rules at the moment; but I have a feeling that's peaking.
Typically, you need to move back and forth a number of times before it clicks. So you have all these people on the net fighting over which end of the spectrum is the Right one, and next month they're on opposite sides.
They're tools, hammers, screw drivers whatever; it doesn't make any kind of sense to identify with them.
Unless your goal is to be a tool, I guess.
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.
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.
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.
Wow wow chill out. It wasn't meant as a negative comment. I was just making the observation most new languages are staticly typed and that a lot of what you hear in the functional space is about types (type theory, dependant types, categories...) though this might be just what I've had infront of me recently. I retract my statement. I love the dynamic functional languages. Erlang and Clojure are amazing (now that I think about it elixir is a lot in the news, as I said my statement probably was wrong).
And as I said in my previous comment, I think Rich talk made some really interesting points.
