[lolski]

I agree with your statement that concepts like formal-proofs is underrated. Fortunately, one of the general trend that I'm seeing going forward is the birth of programming languages with more and more sophisticated type systems. In these languages type systems do not only capture object types (eg., int, string) but also various other aspects.

For example functional languages and their monadic construct supports capturing various interesting aspects. This allows for really useful feature such as capturing concurrency behaviour (Future/Promise) and possibility of returning errors (Try), at compile time.

Then there's Rust where memory ownership can be reasoned about at compile time.

Languages such as Idris allows to declare a type that is dependent on the value (eg., declare that this function "x() can only return odd numbers?)

I also happen to work in a company where we try to bring type-safety to the databse world with our product TypeDB.

I think this trend is very good to see - stronger type-system = safer code. In a way the stronger type system a programming language has, the more it can validate at compile time. And therefore, we can say that such language somewhat provides what formal proof / formal verification systems ought to provide, but in a practical setting.