It's a matter of economics, mostly: proving that a feature is mathematically correct costs a lot more than implementing the feature itself, and so mathematic pr

It's a matter of economics, mostly: proving that a feature is mathematically correct costs a lot more than implementing the feature itself, and so mathematic proofs are not done except if the cost justifies it. And because of that the tools that do these proofs do not take off, and thus they get reinvented every few years with each programming language.