It's a really great concept. What guarantees are made by the prover?

Success in programming languages is not simply if-you-build-it-they-will-come. Bootstrapping a community that loves programming in it is the hard part. You'll either need a killer interop story with an already built ecosystem, or you'll need your own HTTP server, JSON parser, etc. etc. etc.

Best of luck! I'll watch this space.

Thanks! The guarantee is that, without the use of trustme (which can prove any fact), you cannot address memory as the wrong type. The compiler also ensures that a pointer/reference to a value is live at compile time, so it’s not possible to create an invalid pointer (without the use of trustme). You can also claim any fact which the compiler must prove in order to continue compilation.

That is good advice, I’m definitely planning on including some batteries soon, once I’m very happy with where the compiler is at.