On: ZZ is a modern formally provable dialect of C

[Jaxan]

I like how they incorporate an SMT solver. They claim: “all code is proven”. What does that mean? What is proven about the code? Absence of memory bugs, or actual correctness of algorithms?

[mhd → Jaxan]

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

[frabert → Jaxan]

That the code is provably free of C undefined behavior

[MaxBarraclough → frabert]

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

[fuklief → Jaxan]

+1

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

[Jaxan → fuklief]

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.