3 ms·
Author here. fully agree that the description is vague and doesn't really tell you where it stands versus something like F* , SPARK, etc. That's partially beca
by a3p 7y ago
Author here. fully agree that the description is vague and doesn't really tell you where it stands versus something like F* , SPARK, etc.
That's partially because frankly i don't know yet. We'll have to discover slowly how far the first class proof expressions can be pushed.
the word "safe" here is actually gone now, because it indeed says something different. thanks for the feedback.
- MaxBarraclough 7y agoMy pleasure. I've bookmarked the project - I intend to keep an eye on its developments. Am I right in thinking that, as it stands today, ZZ can be used as a rock-solid protection against C's undefined behaviour (in my own code at least), and as a protection against accidentally writing non-portable C code? That's a great starting point, if so.