Mathematically correct is not enough.

Java's byte code verification algorithm had a proof. This was important for running untrusted java in the browser. If it said the byte code was ok, it was.

Turns out, nobody made a proof for the verifier actually finishing. So it could return true, or false, or run longer than the universe has time. So around Java 6(?), someone wrote some bytecode that basically took forever to validate, DOSing the validator. Sun had to change the file format and add extra information to get the guarantees back.

Not the grandparent you were replying to, but from the note added to the original linked issue (emphasis mine):

> Rust's type system is *intended to prevent memory unsafety. Upholding this promise is something we take very seriously*, .... It is a large priority of the Types Team to *fix all type system unsoundnesses* and to work towards there being a solid foundation to minimize the risk of unknown ones.

So, yes, if you have a group who "takes very seriously" the job to "fix all type system unsoundness", I would expect them to utilize some manner of formal proof verification that their type system is mathematically correct up to some defined limit.

No. I am saying you don't need rust for largely correct.

PS: The term you are looking for is formally verified not mathematically proven.