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

151–157 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#151

Post by MaxBarraclough »

loeg wrote: post #116
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…

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

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

Re: ZZ is a modern formally provable dialect of C

#152

Post by loeg »

twsted wrote: post #146
a3p wrote: post #126

Earlier quoted context omitted.

it is https://devguard.io/ which is being rewritten from rust to ZZ in this branch https://github.com/devguardio/carrier/tree/zz

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

Re: ZZ is a modern formally provable dialect of C

#153

Post by Blaisorblade0 »

0xdead wrote: post #143
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 have an anecdote to share. I work in embedded space for a living. A web developer (which is quite funny) from another team somehow convinced our director to use Rust for a critical process that involved a lot of concurrent processing. Ok, I said, and began developing that process in Rust. I estimated that it took me about 10x the time to implement something than it would have taken if I did that in C. The reason fo…

"If it compiles it works" is just not true, just a very bad description for a true phenomenon. If there weren’t people repeating that seriously, you’d be attacking a strawman. People do say that, but that’s on those people, not Rust.

Re: ZZ is a modern formally provable dialect of C

#154

Post by MaxBarraclough »

pjmlp wrote: post #124
MaxBarraclough wrote: post #106

Earlier quoted context omitted.

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

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

Re: ZZ is a modern formally provable dialect of C

#155

Post by steveklabnik »

MaxBarraclough wrote: post #154
pjmlp wrote: post #124

Earlier quoted context omitted.

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.

Re: ZZ is a modern formally provable dialect of C

#157

Post by steveklabnik »

MaxBarraclough wrote: post #156
steveklabnik wrote: post #155

Earlier quoted context omitted.

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.
Post reply on HN