3 ms·
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 provin
by a3p 7y ago
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.
- loeg 7y agoWhat'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/ https://scratch.mit.edu/discuss/topic/80752/
- a3p 7y agoit is https://devguard.io/ https://devguard.io/ which is being rewritten from rust to ZZ in this branch https://github.com/devguardio/carrier/tree/zz https://github.com/devguardio/carrier/tree/zz
- loeg 7y agoThanks!
- twsted 7y agoVery interesting. Can you tell us a little more about the reasons of the rewrite from rust?
- loeg 7y agoI'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).