Hacker News Reader

"Beware of bugs in the above code; I have only proved it correct, not tried it."

That the code is provably free of C undefined behavior

Looking at the example code, [0] it's clear you're correct.

As I just rambled about in another comment in this thread, their project summary isn't clear about this. Still a great idea for a language though.

[0] https://github.com/aep/zz/tree/master/examples/hello/src

+1

What does it even mean that the language is formally provable ?!

To me it means that there is a formal semantics (for example in Coq), and that we can formally prove properties of the code. There does not seem to be a semantics here.