-
Notifications
You must be signed in to change notification settings - Fork 52
FAQ
Answers to recent questions and comments from around the internet.
indeed, smt solving has noticable impact on compile speed. The entire test suite executes in about a minute on a modern machine, but the C compiler part of that is merely 20 seconds, so expect an impact of roughly 3 times as slow as C which is about the same impact as rust or C++.
this is intentionally left vague for now. ZZ is super new, and this will gain meaning as it becomes mature. One thing it means is that it can formally verify the C code is free of "undefined behavior". Of course having only "defined behavior" doesn't mean the program does anything useful. This is why the extremely powerful where/model expressions come into play, allowing you to specify high level proofs of actual functionality.
Here's a high level example with type states: https://github.com/aep/zz/blob/master/examples/taint/src/main.zz
ZZ draws lots of inspiration from lots of things, especially rust, but does not intend to be a competitor. Really the only similar thing to ZZ in terms of features is F*, which is both more mature and more weird.
heap modelling will eventually be implemented. It is simply not a priority right now because currently the biggest user of ZZ is devguard, which works with microcontrollers.
honestly rust is a pretty good language for desktop cli tools. Maybe some day zz will be self-hosted when it becomes more mature.
Some languages take away the responsibility from the programmer by adding runtime checks. ZZ does not. You will still have to think about buffer overflows, but ZZ makes sure you did in fact think about them by forcing you to write a proof. This is more work, but significantly less work than something like coq, because zz can autogenerate a large amount of proofs from the instruction code.
Prove of algorithms is possible as long as there's a known method of doing so in SMT. That means in practice, if someone has written a paper for formally proving an algorithm in SMT, you can mostly copy paste the proof.
Zz is developed in parallel with a large project using zz and new syntax sugar features will surface slowly as they become practically useful.
That being said, it will never replace external formal verification with something like coq. If lives depend on your code, you probably don't want to rely on just zz.
ZZ has no FFI. it is simply a C transpiler. You can freely include any C header, and include ZZ generated C code in other C files. The only thing it cannot do is prove the C code, so you may occasionally need to wrap things in an unsafe {} block. No additional tools are needed to write nodejs modules for example, or put ZZ into your existing embedded toolchain.
This is a major feature and will not change. ZZ will always be C because C is the standard interface for system libraries.
I had no idea. But it is funny, because coq.
it sounds backwards to say that at first, but i do agree with the sentiment. C is the defacto standard system language. That's why ZZ is a C transpiler rather than a new toolchain. You can mix and match it with C or other transpilers as you see fit. It's not a "replace" but rather an "enhance".
Most of the heavy lifting is actually done by the SMT solver, which are backed by hard science. the zz transpilers to C and to SMT are not formally verified, because the language is too much in flux to make the effort worth it yet.
not completely. zz does enforce all api contracts specified with the model keyword, but it doesn't force anyone to add those contracts.
it is thinkable that a community will come up with useful defacto standard contracts, such as the standard err::checked() theory which forces a user of a function to check its error code.