[AstralStorm]

Compiler does not help you. It is not a proof suggestion system like Isabelle/HOL or the like.

In fact error messages rust produces rival the terrible nature of ones in older C++ compilers thus far.

The compiler only prevents you from making mistakes. Intentions do not even enter into it. See, some of the performance critical code in our apps has to work around even the lax C++11 rules. It is completely impossible in rust without using unsafe stuff liberally - specifically gets about 1000x slower and this matters a lot. Compilers know nothing about intentions, nor can a borrow checker enforce intentions unlike a type system.

[burntsushi]

> Compiler does not help you. It is not a proof suggestion system like Isabelle/HOL or the like

This seems like a gratuitous misrepresentation. A compiler does not need a proof suggestion system to help you.

> In fact error messages rust produces rival the terrible nature of ones in older C++ compilers thus far.

No, it doesn't. The error messages are wonderful and constantly improving.

> It is completely impossible in rust without using unsafe stuff liberally - specifically gets about 1000x slower and this matters a lot.

Can you give specific concrete examples?