4 ms·
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 actu
by Jaxan 7y ago
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 7y ago"Beware of bugs in the above code; I have only proved it correct, not tried it."
- fuklief 7y ago+1 What does it even mean that the language is formally provable ?!
- Jaxan 7y agoTo 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.
- frabert 7y agoThat the code is provably free of C undefined behavior
- MaxBarraclough 7y agoLooking 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 https://github.com/aep/zz/tree/master/examples/hello/src