I wouldn't disagree that dependent types are great for certain specialised problem domains, but they've already been around for ages and didn't yet revolutionise the world of software design. I think the sentiment that this is unlikely to make a big splash is totally on point. Languages have to balance ease of use with features in order to become very popular. Nothing as purebred as Haskell is likely to become the next Python or Visual Basic. Real work horses are dirty, messy machines. Of course this new feature might turn out to be popular for Haskell users.

>but they've already been around for ages and didn't yet revolutionise the world of software design.

I think it's mostly because languages with dependent types are awfully clunky to use. Perhaps dependent typing is even a dead end, but I wouldn't count out other ideas such as refinement typing just yet. I think it will take a lot of work and failed attempts (such as typestate in early Rust) to get fancy type theory into mainstream languages (just like it took a while for Java to get lambdas).

Case in point: static analysis tools for C++ are getting more capable and popular recently.

Formal methods in general are extremely clunky to use. Just see how much hate Rust gets for making it extremely difficult to make an intrusive linked list. And memory safety is only one kind of correctness assertion.

So I'm gonna be a pessimist here and say: nope, not gonna be the future, because programmers are lazy and "ship it now" is better than "prove the bugs don't exist".

Not all programmers build WordPress plugins.

Some programmers write software for aircraft. The "ship it now" maxim doesn't exist in that context.

No one is writing aircraft software in Haskell. They need good control over memory usage.

Counter-example: https://smaccmpilot.org/software/index.html

Also, a Haskell DSL for automotive control systems: http://tomahawkins.org/

That isn't a counter-example unless you're taking his post literally. In which case I claim that Python is a system programming language because one time somebody somewhere wrote a driver in it.

Well... for 95-99%[1] of all software being written, "ship it now" beats "prove that bugs don't exist". Better formal methods could really help that 1-5%, but they're not going to impact the 95% very much.

[1] All statistics made up on the spot. I think it's in the right ballpark, though.

The cpp static analysis tools are all wildly unsound. This is a core design principle behind all real world deployable static analysis systems, whether they are based on abstract interpretation or model checking or symbolic execution, or anything else.

Static analysis is a powerful technique. But sound formal methods have been failing to make a splash for nearly five decades.

Honestly, I'd be happy with a language that can propagate the result of a conditional statement into compile-time constraints inside the branches, and also can create executables without jumping through 20 hoops.

The thing about Haskell is you shouldn’t consider it a finished product. Yes, there are people using it and their experience is invaluable, but it’s also a huge research project into what a programming language could look like. It isn’t mainstream ready yet, but you can see the future come into view.

On the other hand, even those messy real work horses have been adopting functional programming features at a rapid pace over the past decade or two. And many of those features originate from Haskell.

> and didn't yet revolutionise the world of software design

Well, they have. There's a reason why the companies who have adopted these technologies have adopted them.

The future is here, it's just not evenly distributed.

But why dependent types and not one of the many other formal methods that have been around for decades? Especially given the trend towards compilation speed being a relevant design choice (e.g., golang).

Sound global formal verification largely sucks. Type checking is about as far as we've ever gotten using it for widespread real world applications, and most type checkers in major languages are only "sound-y".