On: The struggle with Rust

[gravypod]

Yes that is exactly what I'd like but I'd like something that's grown past just type checking. There are many more bugs that I know can be caught by a theorem prover.

Edit: I want to clarify. I think just type checking should be written as "Just type checking".

[AstralStorm → gravypod]

Indeed, something like what is being tried in Pyret to make contracts (a kind of theorem lemma) the first class citizen.

[junke → gravypod]

As a matter of fact, I agree.