In the last decade or so there has been an explosion in the popularity of explicitly typed languages. Typescript, typed python, Rust with its very strict and expressive type system, etc. That's not full formal proofs of the entire behavior, but it's a solid step back in that direction.
Imho any change in this direction is predicated on tooling and developer experience. Explicit typing was made easier by smarter autocomplete from better IDE plugins, and those same plugins make more valuable suggestions if you have better types, creating a virtuous circle.
Nothing of the form exists so far for formal proofs. If you limit it to small sections of behavior it might pass as a smart but obscure way to write unit tests (ensuring that certain behaviors hold). But nothing outside of your unit tests benefits from it.
Maybe making the specification the starting point from which an LLM writes code changes that. But so far all the evidence points to people being very bad at writing specifications and preferring imperative over declarative languages.
> Rust with its very strict and expressive type system
Tangentially, I find it very interesting how Rust could have had fully inferred types (like OCaml does), but chose to require specifying types at function boundaries.
It shows a thoughtful balance of what the system can technically do, and what's actually useful to the humans dealing with the code.
Rust doesn’t have a very expressive type system. Rust type system would have been at home twenty years ago. Ocaml already had a better type system when I used it professionally in the 2010s and they have added a lot since and you could already type infer everything.
I’m sorry but implying that having typing becoming a bit more popular is a significant step towards formal proof is akin to saying we are getting closer to using efficient heating because we have switched from burning peat to coal.
Imho any change in this direction is predicated on tooling and developer experience. Explicit typing was made easier by smarter autocomplete from better IDE plugins, and those same plugins make more valuable suggestions if you have better types, creating a virtuous circle.
Nothing of the form exists so far for formal proofs. If you limit it to small sections of behavior it might pass as a smart but obscure way to write unit tests (ensuring that certain behaviors hold). But nothing outside of your unit tests benefits from it.
Maybe making the specification the starting point from which an LLM writes code changes that. But so far all the evidence points to people being very bad at writing specifications and preferring imperative over declarative languages.