When i was the focus of the rust community, and trending #1 on HN, i simply deleted my repos and disappeared.

Some people in that community reflexively see a conspiracy or invoke the CoC or use whatever other non technical tools they find to derail the discussion.

It's not even that they're always wrong or that I directly oppose the culture they want to have, but the shotgun blast of drama that this comes with is just so much effort to navigate that i decided to just never contribute to rust again.

Absolutely! The zz export command just dumps the C and SMT code along with makefiles for common build systems and stops there. Very handy for using it within other toolchains.

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.

My 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.

the standard library does not allocate any heap memory, but heap modelling will be added to the prover eventually.

note that there are convenience tools to deal with heap-free targets (microcontrollers) such as tail variants (statically enforced flexible arrays):

https://github.com/aep/zz#metaprogramming-or-templates-tail-...

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. They serve a different purpose.

What's the large project using ZZ? Or is it behind closed doors? This appears to be an entirely different ZZ programming language: https://scratch.mit.edu/discuss/topic/80752/

it is https://devguard.io/ which is being rewritten from rust to ZZ in this branch https://github.com/devguardio/carrier/tree/zz

Very interesting.

Can you tell us a little more about the reasons of the rewrite from rust?

I'm not involved, but one obvious answer is: broader portability than Rust (this is explicitly called out in the ZZ article). Clearly devguard is targetting a broader set of devices than the limited set Rust currently targets (x86; arm, mips, riscv in tier 2, with various caveats for bare metal targets).

Thanks!

that is correct. however, zz does enforce api contracts which can be arbitrary expressions within the QF_UFVB theory.

for example check out the err::checked() theory which enforces that a function call must be followed by err::check.

similarly, i expect a community will come up with other standard contracts such as must_not_copy() for secret values that may not be copied.