Provable properties for cryptographic algorithms is a thing. Provably correct compilers exist. It’s not hard to imagine provably correct kernel modules for example and benefits they’d bring. If they had better ux you could imagine business logic, state machines, asynchronous computation to have provable properties as well. It’s very interesting area but on the edge of usability currently. I’d predict it has great future as ai gets incorporated more and more as it gives solid logic/mathematical proofs over solutions - if it doesn’t make sense to you, think json schema like validated llm output but for any computation.

Sophisticated programming languages dive towards this direction already compared to untyped cousins. Programs are validated against type theory correctness. You can go deeper with dependent types. And those languages go all the way down to prove everything there is to be proven.