Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

ZZ is a modern formally provable dialect of C

github.com

Post reply on HN
Print view View original

101–110 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#101

Post by quotemstr »

scoutt wrote: post #5

> where we still program C out of desperation I agree it's the standard and the only thing that actually works (author's words), but it's still a pleasure for me to write and have to deal with C (for embedded). I'd be desperate if I have to be forced to deal with huge different paradigms because pointer problems or insert-your-C-rant-here . C is not going to be replaced on embedded any moment soon.

> I agree it's the standard and the only thing that actually works (author's words),

C++ also "actually works" and, thanks to its much greater ability to support fluent abstractions, ends up being safer in practice than raw C code. You can use C++ for low-level system components. Did you know Android's libc is actually written in C++?

Re: ZZ is a modern formally provable dialect of C

#102

Post by AnimalMuppet »

michaelt wrote: post #84
dmos62 wrote: post #20

Earlier quoted context omitted.

> C is not going to be replaced on embedded any moment soon. Why? Doesn't for example Rust without stdlib already cover the use cases? Note I'm not experienced in embedded.

C's strength is the ecosystem: * Your microprocessor has a C compiler and standard library, as does every processor you might ever switch to. All the hardware documentation that isn't tables in a PDF will be in C. * Your target's static analysis tools and interactive debuggers will all support C. * Every RTOS and embedded library/filesystem/whatever will support (and likely be written in) C. * All experienced embedde…

> The disadvantages of C are many and well known.

Which, in a way, is an advantage. I know (much of) what to look out for. There are tools that can help me with some of those issues. There are techniques that avoid some of them, and there are people who are expert in many of them.

But if I pick some other language, it won't have those problems. It will have other problems. (There is no language that does not have problems.) I won't know what to avoid doing. There may not be tooling to help with them. The techniques for avoiding them may not be widely known. I may not be able to find people who know how to handle them.

To me, "well known problems" may be better than "not well known problems". More predictable, at least. The "not well known" problems have to be significantly better to be worth it. They probably have to be proven significantly better. That means either that someone else has to prove them better, or else I have to have a project that doesn't matter much that I can use as a testbed.

Re: ZZ is a modern formally provable dialect of C

#103

Post by augusto-moura »

lwb wrote: post #90
augusto-moura wrote: post #88

Earlier quoted context omitted.

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?

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

Re: ZZ is a modern formally provable dialect of C

#104

Post by pickdenis »

iainmerrick wrote: post #100

One question that isn’t obvious from the overview: This language compiles to C and asserts that your program will never exhibit undefined behavior; have they proved that ZZ is correct , ie that it will definitely never output C code that exhibits undefined behavior? If you really care about correctness, that seems important. I absolutely love the idea in general though.

This seems similar to bootstrapping theorem provers. Here is a HN discussion on one: https://news.ycombinator.com/item?id=21358674

Re: ZZ is a modern formally provable dialect of C

#105

Post by augusto-moura »

MaxBarraclough wrote: post #92
augusto-moura wrote: post #88

Earlier quoted context omitted.

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

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 prog…

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

Re: ZZ is a modern formally provable dialect of C

#106

Post by MaxBarraclough »

MaxBarraclough wrote: post #79

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 ne…

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

Re: ZZ is a modern formally provable dialect of C

#107

Post by MaxBarraclough »

augusto-moura wrote: post #105
MaxBarraclough wrote: post #92

Earlier quoted context omitted.

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 prog…

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.

Re: ZZ is a modern formally provable dialect of C

#108

Post by a3p »

augusto-moura wrote: post #105
MaxBarraclough wrote: post #92

Earlier quoted context omitted.

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 prog…

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

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.

Re: ZZ is a modern formally provable dialect of C

#109

Post by a3p »

MaxBarraclough wrote: post #97
pickdenis wrote: post #95

Earlier quoted context omitted.

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

Re: ZZ is a modern formally provable dialect of C

#110

Post by zozbot234 »

MaxBarraclough wrote: post #107
augusto-moura wrote: post #105

Earlier quoted context omitted.

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 pr…

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

Post reply on HN