4 ms·

> Your language does not allow me to prove program correctness Isn't that the whole point of the SMT solver? What about this example (that doesn't compile)?

> Your language does not allow me to prove program correctness Isn't that the whole point of the SMT solver? What about this example (that doesn't compile)? fn bla(int a) -> int model return == 2 * a { return a * a; } Isn't that verifying program correctness? A sibling of this comment claims that "the only thing proven is memory access validity" but, again, this example takes that down.

MaxBarraclough 7y ago
I agree that it is. Looking at the page, I can't see how far this goes. Was my earlier comment completely wrong? Does ZZ allow the programmer to express a formal specification, e.g. to verify a sort function? If so, their examples are selling their language very short.
- 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 ago
    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/ https://scratch.mit.edu/discuss/topic/80752/
    - a3p 7y ago
      it 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 ago
        Thanks!
      - twsted 7y ago
        Very interesting. Can you tell us a little more about the reasons of the rewrite from rust?
        loeg 7y ago
        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).
a1369209993 7y ago
> > program correctness How would this language (or any other) go about verifying the correctness of: fn subtract(int a,int b) -> int model return == a + b { return a + b; }
- MaxBarraclough 7y ago
  This defect is obvious to anyone reviewing the code, and it will be even more obvious when the function is used by another function with its own contracts. In practice the issue with formal modelling is that it's very hard to scale up. Modelling the correct behaviour of traffic-lights is practical, and allows us to build completely bug-free traffic-light software, but these methods don't work so well for developing a word processor. Competent practitioners don't tend to mess up their formal models though. I've not heard an example of that causing defective software, but it's a valid question to ask. Even without going the whole way to whole-program correctness guarantees, this kind of approach can be used to provide solid guarantees against bugs like buffer-overflows, without using runtime checks. This is something the SPARK language has supported for a long time.

MaxBarraclough 7y ago

I agree that it is. Looking at the page, I can't see how far this goes. Was my earlier comment completely wrong? Does ZZ allow the programmer to express a formal specification, e.g. to verify a sort function? If so, their examples are selling their language very short.

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 ago
  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/ https://scratch.mit.edu/discuss/topic/80752/
  - a3p 7y ago
    it 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 ago
      Thanks!
    - twsted 7y ago
      Very interesting. Can you tell us a little more about the reasons of the rewrite from rust?
      - loeg 7y ago
        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).

a1369209993 7y ago

> > program correctness How would this language (or any other) go about verifying the correctness of: fn subtract(int a,int b) -> int model return == a + b { return a + b; }

MaxBarraclough 7y ago
This defect is obvious to anyone reviewing the code, and it will be even more obvious when the function is used by another function with its own contracts. In practice the issue with formal modelling is that it's very hard to scale up. Modelling the correct behaviour of traffic-lights is practical, and allows us to build completely bug-free traffic-light software, but these methods don't work so well for developing a word processor. Competent practitioners don't tend to mess up their formal models though. I've not heard an example of that causing defective software, but it's a valid question to ask. Even without going the whole way to whole-program correctness guarantees, this kind of approach can be used to provide solid guarantees against bugs like buffer-overflows, without using runtime checks. This is something the SPARK language has supported for a long time.