7 ms·

I find the basic idea of this project to be very compelling - I was thinking aloud on HN recently and arrived at roughly the idea this project is implementing.

I find the basic idea of this project to be very compelling - I was thinking aloud on HN recently and arrived at roughly the idea this project is implementing. [0] With that said, I really dislike the way they're describing their project. When I read safe dialect of C, I first assumed they meant they had developed a safe subset of C, or perhaps a very similar language, like OpenCL C [1]. Instead, they developed a new language which isn't C at all. Nothing wrong with that, but if I don't instantly recognise the syntax as C, I wouldn't call it a C dialect. They also put formally provable dialect of C. Their language compiles to C code which is guaranteed to be free from undefined behaviour. This is not the same thing as a language where hard guarantees can be made about program behaviour, such as SPARK [2] or Dafny [3]. If the authors are reading this, I urge you to improve your project summary. Your language does not allow me to prove program correctness, instead it protects me from C's undefined behaviour. That's still a great idea! Please make this clear! [0] https://news.ycombinator.com/item?id=22102658 https://news.ycombinator.com/item?id=22102658 [1] https://en.wikipedia.org/wiki/OpenCL#OpenCL_C_language https://en.wikipedia.org/wiki/OpenCL#OpenCL_C_language [2] https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) [3] https://en.wikipedia.org/wiki/Dafny https://en.wikipedia.org/wiki/Dafny

lwb 7y ago
Seems like they are using a narrow definition of "mathematically provable" -- they only thing that appears to be proven is that "all memory access is mathematically proven to be defined". Which just seems like a fancy way of achieving the same thing as a type checker? Either way, cool project, but is there anything else that ZZ can prove?
- augusto-moura 7y ago
  In the README there's a example of proving a simple state machine open > read > close [1] Just read the docs™ [1] https://github.com/aep/zz#theory https://github.com/aep/zz#theory
  - lwb 7y ago
    Ah ok, not sure how I missed that. That still seems to be within the realm of a type system, no? Or would you consider type systems a subset of mathematically provable systems?
    - ludamad 7y ago
      Dependent type systems certainly are!
    - augusto-moura 7y ago
      Well Type Theory is actually one of the definitions of mathematics and computation[1]. Wikipedia gives a basic definition of it [2][3] [1] https://en.wikipedia.org/wiki/Typed_lambda_calculus https://en.wikipedia.org/wiki/Typed_lambda_calculus [2] https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [3] https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics
  - MaxBarraclough 7y ago
    So it has typestates. (I recommend anyone [0] and its HN thread [1] for detail.) I think that's a great language feature for helping to avoid bugs, especially the kind that often happen in C, but I don't imagine it's anywhere close to proving whole-program correctness, is it? For the curious, here's an official example in the SPARK language, that gives a proven-correct sort function. (A complete proof of correct program behaviour, not just absence of undefined behaviour). As you can see, proving correctness is a challenge that permeates every inch of the code. [2][3] Microsoft's Dafny language is similar. [4] [0] https://yoric.github.io/post/rust-typestate/ https://yoric.github.io/post/rust-typestate/ [1] https://news.ycombinator.com/item?id=21413174 https://news.ycombinator.com/item?id=21413174 [2] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.ads https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [3] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.adb https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [4] https://en.wikipedia.org/wiki/Dafny#Imperative_features https://en.wikipedia.org/wiki/Dafny#Imperative_features
pickdenis 7y ago
> 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
deleted 7y ago
[deleted]
MaxBarraclough 7y ago
(A now-deleted comment said it's disappointing that ZZ doesn't support whole-program correctness-proofs. I'll hang my reply here rather than delete it.) I should point out it's possible I completely misread the project summary. Perhaps it does support that after all. [0] I still like the idea though, and might try it out at some point. There's a lot of value in guaranteeing no undefined-behaviour in my code. Imagine how much more secure our systems would be if they had these guarantees. There's also a lot of value in transpiling to portable, standard-compliant C code. If you want a language that supports full proof-of-correctness, we do already have SPARK and Dafny, but they're no walk in the park. I'm an optimist about this though - I think they'll continue to slowly get more approachable. A brief aside: SPARK strikes me as already being more approachable than the Event-B formal specification language, which starts with the formal specification in math (set theory), and ends in imperative code (after 'refining' the model into an implementation). That's despite that Event-B is a more approachable derivative of B-Method, itself a more approachable alternative to Z Notation. Annoyingly I couldn't find a great one-page summary to give the flavour of Event-B (there are a lot of beautifully crafted PDFs, as it's from academia), the best I can do is [1]. [0] https://news.ycombinator.com/item?id=22249135 https://news.ycombinator.com/item?id=22249135 [1] https://www3.hhu.de/stups/handbook/rodin/current/html/tut_building_the_model.html https://www3.hhu.de/stups/handbook/rodin/current/html/tut_bu...
- pjmlp 7y ago
  I think NVidia's adoption of SPARK for security critical firmware is victory, specially since they also evaluated Frama-C and Rust as part of their selection process. Rust probably would have made it in the future, but it is still not mature enough to the domains NVidia intends to use SPARK on. https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-autonomous-driving/ https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto...
  - MaxBarraclough 7y ago
    Rust isn't aiming for formal verification, is it?
loeg 7y ago
It seems like the pre- and post-conditions could be used to prove program correctness?
- MaxBarraclough 7y ago
  Yes, see a3p's comments. I was mistaken.
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 ago
  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.

lwb 7y ago

Seems like they are using a narrow definition of "mathematically provable" -- they only thing that appears to be proven is that "all memory access is mathematically proven to be defined". Which just seems like a fancy way of achieving the same thing as a type checker? Either way, cool project, but is there anything else that ZZ can prove?

augusto-moura 7y ago
In the README there's a example of proving a simple state machine open > read > close [1] Just read the docs™ [1] https://github.com/aep/zz#theory https://github.com/aep/zz#theory
- lwb 7y ago
  Ah ok, not sure how I missed that. That still seems to be within the realm of a type system, no? Or would you consider type systems a subset of mathematically provable systems?
  - ludamad 7y ago
    Dependent type systems certainly are!
  - augusto-moura 7y ago
    Well Type Theory is actually one of the definitions of mathematics and computation[1]. Wikipedia gives a basic definition of it [2][3] [1] https://en.wikipedia.org/wiki/Typed_lambda_calculus https://en.wikipedia.org/wiki/Typed_lambda_calculus [2] https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [3] https://en.wikipedia.org/wiki/Foundations_of_mathematics https://en.wikipedia.org/wiki/Foundations_of_mathematics
- MaxBarraclough 7y ago
  So it has typestates. (I recommend anyone [0] and its HN thread [1] for detail.) I think that's a great language feature for helping to avoid bugs, especially the kind that often happen in C, but I don't imagine it's anywhere close to proving whole-program correctness, is it? For the curious, here's an official example in the SPARK language, that gives a proven-correct sort function. (A complete proof of correct program behaviour, not just absence of undefined behaviour). As you can see, proving correctness is a challenge that permeates every inch of the code. [2][3] Microsoft's Dafny language is similar. [4] [0] https://yoric.github.io/post/rust-typestate/ https://yoric.github.io/post/rust-typestate/ [1] https://news.ycombinator.com/item?id=21413174 https://news.ycombinator.com/item?id=21413174 [2] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.ads https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [3] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug/gnatprove_by_example/examples/sort.adb https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [4] https://en.wikipedia.org/wiki/Dafny#Imperative_features https://en.wikipedia.org/wiki/Dafny#Imperative_features

pickdenis 7y ago

> 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

deleted 7y ago

[deleted]

MaxBarraclough 7y ago

(A now-deleted comment said it's disappointing that ZZ doesn't support whole-program correctness-proofs. I'll hang my reply here rather than delete it.) I should point out it's possible I completely misread the project summary. Perhaps it does support that after all. [0] I still like the idea though, and might try it out at some point. There's a lot of value in guaranteeing no undefined-behaviour in my code. Imagine how much more secure our systems would be if they had these guarantees. There's also a lot of value in transpiling to portable, standard-compliant C code. If you want a language that supports full proof-of-correctness, we do already have SPARK and Dafny, but they're no walk in the park. I'm an optimist about this though - I think they'll continue to slowly get more approachable. A brief aside: SPARK strikes me as already being more approachable than the Event-B formal specification language, which starts with the formal specification in math (set theory), and ends in imperative code (after 'refining' the model into an implementation). That's despite that Event-B is a more approachable derivative of B-Method, itself a more approachable alternative to Z Notation. Annoyingly I couldn't find a great one-page summary to give the flavour of Event-B (there are a lot of beautifully crafted PDFs, as it's from academia), the best I can do is [1]. [0] https://news.ycombinator.com/item?id=22249135 https://news.ycombinator.com/item?id=22249135 [1] https://www3.hhu.de/stups/handbook/rodin/current/html/tut_building_the_model.html https://www3.hhu.de/stups/handbook/rodin/current/html/tut_bu...

pjmlp 7y ago
I think NVidia's adoption of SPARK for security critical firmware is victory, specially since they also evaluated Frama-C and Rust as part of their selection process. Rust probably would have made it in the future, but it is still not mature enough to the domains NVidia intends to use SPARK on. https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-autonomous-driving/ https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-auto...
- MaxBarraclough 7y ago
  Rust isn't aiming for formal verification, is it?

loeg 7y ago

It seems like the pre- and post-conditions could be used to prove program correctness?

MaxBarraclough 7y ago
Yes, see a3p's comments. I was mistaken.

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