Some type systems (e.g, Haskell) are closing in in becoming formal verification languages themselves.

Piggybacking off your comment, I just completed a detailed research paper where I compared Haskell to C# with an automated trading strategy. I have many years of OOP and automated trading experience, but struggled a bit at first implementing in Haskell syntax. I attempted to stay away from LLMs, but ended up using them here and there to get the syntax right.

Haskell is actually a pretty fun language, although it doesn't fly off my fingers like C# or C++ does. I think a really great example of the differences is displayed in the recursive Fibonacci sequence.

In C#:

    public int Fib(int n)
    {
        if (n <= 1)
            return n;
        else
            return Fib(n - 1) + Fib(n - 2);
    }
In Haskell:

    fib :: Integer -> Integer
    fib n
      | n <= 1    = n
      | otherwise = fib (n - 1) + fib (n - 2)
As you might know, this isn't even scratching the surface of the Haskell language, but it does a good job highlighting the syntax differences.

When using switch expression in C#, they are a lot more similar:

    public int Fib(int n) => n switch
    {
        <= 1 => n,
        _    => Fib(n - 1) + Fib(n - 2)
    };

And one can see how quickly they became mainstream...

Given that it's the AI doing the coding, it would be pretty quickly so long as it's decent at Haskell. Which it already is, surprisingly so actually for such a niche language. It doesn't necessarily write great code, but it's good enough, and the straightjacket type system makes it very hard for the model to sneak in creative hacks like using globals, or trip itself with mutable state.

I think that’s because the barrier to entry for a beginner is much higher than say python.

IMHO, these strong type systems are just not worth it for most tasks.

As an example, I currently mostly write GUI applications for mobile and desktop as a solo dev. 90% of my time is spent on figuring out API calls and arranging layouts. Most of the data I deal with are strings with their own validation and formatting rules that are complicated and at the same time usually need to be permissive. Even at the backend all the data is in the end converted to strings and integers when it is put into a database. Over-the-wire serialization also discards with most typing (although I prefer protocol buffers to alleviate this problem a bit).

Strong typing can be used in between those steps but the added complexity from data conversions introduces additional sources of error, so in the end the advantages are mostly nullified.

> Most of the data I deal with are strings with their own validation and formatting rules that are complicated and at the same time usually need to be permissive

this is exactly where a good type system helps: you have an unvalidated string and a validated string which you make incompatible at the type level, thus eliminating a whole class of possible mistakes. same with object ids, etc.

don't need haskell for this, either: https://brightinventions.pl/blog/branding-flavoring/

That's neat, I was about to ask which languages support that since the vast majority don't. I didn't know that you can do that in Typescript.

Any language with an type system really...

Even OOP : if you have a string class, you can have a String_Formated_For_API subtype.

Just extends String, and add some checking.

But now the type checker "knows" it can print() a String_Formated_For_API just fine but not call_API(string).

I would argue that the barrier to entry is on par with python for a person with no experience, but you need much more time with Haskell to become proficient in it. In python, on the other hand, you can learn the basics and these will get you pretty far

Python has a reputation for being good for beginners so it's taught to beginners so it has a reputation for being good for beginners.

I blame syntax. It's too unorthodox nowadays. Historical reasons don't matter all that much, everything mainstream is a C-family memember