Conflating types in binary operations hasn't been an issue for me since I started using TS in 2016. Even before that, it was just the result of domain modeling done badly, and I think software engineers got burned enough for using dynamic type systems at scale... but that's a discussion to be had 10 years ago. We all moved on from that, or at least I hope we did.

> Now we all should be looking towards fail-safe systems, formal verification and domain modeling.

We were looking forward to these things since the term distributed computing has been coined, haven't we? Building fail-safe systems has always been the goal since long-running processes were a thing.

Despite any "past riddles", the more expressive the type system the better the domain modeling experience, and I'd guess formal methods would benefit immensely from a good type system. Is there any formal language that is usable as general-purpose programming language I don't know of? I only ever see formal methods used for the verification of distributed algorithms or permission logic, on the theorem proving side of things, but I have yet to see a single application written only in something like Lean[0] or LiquidHaskell[1]...

[0]: https://lean-lang.org/

[1]: https://ucsd-progsys.github.io/liquidhaskell/