> 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

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