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!
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].
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.
> 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.
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).
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?
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]
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
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.
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?
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
[1] https://en.wikipedia.org/wiki/OpenCL#OpenCL_C_language
[2] https://en.wikipedia.org/wiki/SPARK_(programming_language)
[3] https://en.wikipedia.org/wiki/Dafny