Comment by whilenot-dev
19 days ago
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]...
I think the only people who burnt of the discussion were people who is terminally online. But in the industry, there is people in any paradigm with any previous development times you can remember of.
> Is there any formal language that is usable as general-purpose programming language I don't know of?
That’s sort of my point, the closest thing to a rich type system yet pragmatic enough is to me F# and it’s still falls short as formal verification and ecosystem integration.
I think eventually, we should invest into this direction so LLM production can be trusted, or even ideally, producing or helping with the specific specifications of models. This is yet to be done.
I don’t want to make a prophecy, but the day, ergonomics and verification meet in an LLM automated framework, this new development environment should take over everything previous.