No mention of unions, discriminated or otherwise. Sums/unions are a pretty important abstraction, and a lot of C's unsafety can sneak in if you don't enforce discriminated unions.
ZZ is a modern formally provable dialect of C
121–130 of 157 posts
Re: ZZ is a modern formally provable dialect of C
#122Earlier quoted context omitted.
While C isn't going to replaced on embedded any moment soon, there are alternatives out there, when the team is open minded. C++, Pascal, Basic, Java, Ada, Oberon all have mature toolchains available from companies that have been in business for the last couple of decades. As per several C++ retrospective talks, the focus on C is more social issue than anything else.
> As per several C++ retrospective talks, the focus on C is more social issue than anything else. The social issue may be that many embedded programmers prefer C to C++, for what they believe to be legitimate reasons.
Most of which seem more like cargo cult than anything else.
Re: ZZ is a modern formally provable dialect of C
#123Earlier quoted context omitted.
On most (small, I'm not talking about mini linux) embedded systems, instruction counting will tell you how long something takes to run. In fact, the compilers available are often so primitive that operation counting in the source code can sometimes tell you how long something will take.
On most embedded ARM it won't (out of order execution, caches, alignment), and they don't have to run Linux, likewise on common MIPS implementations. Simple predictability ends at 16-bit CPUs generally, and even those can be tricky if it's say m68k.
"Most" embedded ARM? Cortex-A8 and smaller do not have OoO execution. Cortex-A9 is a 32-bit up-to-quad core CPU with clock of 800MHz-2GHz and 128k-8MB of cache. That's pretty big. I guess a lot of this is subject to opinion, but I don't think smartphones with GBs of RAM when I think of embedded systems.
Re: ZZ is a modern formally provable dialect of C
#124I 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…
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...
Re: ZZ is a modern formally provable dialect of C
#125> 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++?
Windows new one as well.
Re: ZZ is a modern formally provable dialect of C
#126Earlier quoted context omitted.
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 ve…
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
Re: ZZ is a modern formally provable dialect of C
#127This is just another symptom of why OpenSource often sucks. Instead of somehow coordinating and focusing their efforts, everyone seems to need to start their own spin off "inspired" by other projects. When do people realize that building a new language is almost always going to fail and only very very few languages ever reach anything close to adoption. Instead of spending all this time writing your own doomed langua…
Bjarne Stroustrup never expected C++ to be very widely used. He made it anyway.
Alex Stepanov never thought that anyone would care about his ideas on generic programming. He pursued them anyway. They became the STL.
True, building a new language is almost always going to fail. The problem is, when someone starts working on a new language, they don't know if it's doomed or not. It is good that 1000 people try, because from that we get one language that many people use, and 10 specialized languages that a few people use, and 10 languages that nobody uses but future people steal some of the ideas.
> The same goes for Linux, which is the paradigm of wasted efforts.
Um... what? Wasted because nobody uses it? Very much no. Wasted because it's a duplication of what was there before? To some degree, yes. But not everything in Linux was in Unix before it. And Unix couldn't run all the places that Linux does (smartphones to mainframes). So, no, Linux is not wasted effort.
Re: ZZ is a modern formally provable dialect of C
#128Earlier quoted context omitted.
> 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.
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.
Re: ZZ is a modern formally provable dialect of C
#129I 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…
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.
Re: ZZ is a modern formally provable dialect of C
#130Earlier quoted context omitted.
On most (small, I'm not talking about mini linux) embedded systems, instruction counting will tell you how long something takes to run. In fact, the compilers available are often so primitive that operation counting in the source code can sometimes tell you how long something will take.
On most embedded ARM it won't (out of order execution, caches, alignment), and they don't have to run Linux, likewise on common MIPS implementations. Simple predictability ends at 16-bit CPUs generally, and even those can be tricky if it's say m68k.
When I hear "embedded ARM", I hear "Cortex M".
All of Cortex M is in-order and only M7-- still somewhat exotic-- has a real cache (silicon vendors often do some modest magic to conceal flash wait states, though).
Alignment requirements are modest and consequences are predictable. Etc.
About the most complicated performance management thing you get is the analysis of fighting over the memory with your DMA engine. And even that you can ignore if you're using a tightly coupled memory...