Hacker News Reader

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.

(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

[1] https://www3.hhu.de/stups/handbook/rodin/current/html/tut_bu...

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

Rust isn't aiming for formal verification, is it?

It’s something we’d like and are vaguely pursuing but not at the expense of other things.

Neat, thanks.

No problem. “Rust Belt” and “Miri” are the terms to search for if you want to learn more.

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

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.

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

Thanks!

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

> > 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;
    }

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.

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?

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

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?

Dependent type systems certainly are!

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

[2] https://en.wikipedia.org/wiki/Type_theory

[3] https://en.wikipedia.org/wiki/Foundations_of_mathematics

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/

[1] https://news.ycombinator.com/item?id=21413174

[2] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug...

[3] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug...

[4] https://en.wikipedia.org/wiki/Dafny#Imperative_features

I imagine that whole-program correctness can be represented, but is not enforced in the case of ZZ. Developers are not obligated to declare typesets for their own code or can rely on other libraries being fully typed

> not enforced in the case of ZZ

I don't think it's really even possible for a language to force the programmer to give a proper formal specification.

We may want the formal spec to grant some leeway, i.e. not to specify the exact output/behaviour, but instead to express certain important constraints. For instance, we may not care which traffic-light turns green first, so long as the system preserves the important properties about safety and liveness.

If we wish to support such flexibility, we can't stop the programmer from expressing all output states are valid.

If we don't wish to support such flexibility, what we're really doing is comparing against a reference implementation.

> I don't think it's really even possible for a language to force the programmer to give a proper formal specification.

The language, probably not. The standard library can certainly require detailed-enough formal preconditions to make its code defect-free, meaning that any remaining bugs can then be directly traced to the programmer's code.

You mean that, for instance, a standard-library generic sort function, might require that your comparator function behave correctly when the arguments are reversed?

That's an interesting idea. Like Java interfaces, but with formal contracts.

I doubt that putting these contracts into the standard-library would give you good proof-coverage though.

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.

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

Yes, see a3p's comments. I was mistaken.