[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?