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

131–140 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#131

Post by mlyle »

loeg wrote: post #123
AstralStorm wrote: post #78

Earlier quoted context omitted.

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.

Even e.g. A53 is in-order, and it's a 64 bit, pretty quick CPU (as seen in Raspberry Pi 2/3).

Re: ZZ is a modern formally provable dialect of C

#133

Post by boomlinde »

oblio wrote: post #38
scoutt wrote: post #31

Earlier quoted context omitted.

The answer is size, power consumption and most of all, price. I know I can do a wrist watch with a Raspberry Pi, but will it be profitable/convenient?

Well, let's say I take the Intel P54 ( https://en.wikipedia.org/wiki/List_of_Intel_microprocessors#... ) as an example. So basically an Intel Pentium from 1994, so from 26 (!) years ago. Size: 90 mm2, maximum power consumption: 10W, price at launch: $699. Buuuut: production process 600nm. Today every Intel CPU uses a 14nm production process, but let's go for a cheaper option and "use" the 22nm. So the gate size is ~3…

You are very nearly talking about the Intel Quark. They weren't very popular and Intel have since discontinued the line.

Re: ZZ is a modern formally provable dialect of C

#134

Post by Gene_Parmesan »

speps wrote: post #18
simias wrote: post #12

Earlier quoted context omitted.

I'd expect that a formally provable language would be more complicated to write in practice than Rust. Take this example for instance: >you must tell the compiler that accessing the array at position 2 is defined. quick fix for this one: fn bla(int * a) where len(a) == 3 { a[2]; } In Rust you don't need the where clause, the `a[2]` operation will just panic at runtime if the array is too short. You don't have to prov…

Except the checks in ZZ are at compile time and have no runtime overhead.

Right, but the question was about which language was more complicated (with the implication being, complicated to write). In that sense I think my GP comment is probably correct.

Re: ZZ is a modern formally provable dialect of C

#135

Post by mypalmike »

scoutt wrote: post #58
hurrrrrrrr wrote: post #52

Earlier quoted context omitted.

But if we get rid of a whole class of bugs and vulnerabilities, the number of bugs will go down, no?

This is a common way of thinking about it, but nobody really knows. It's purely a conjecture. There is no data to back it up, and it just appeals to common sense. Should everybody drop C/C++/whatever and rush into the Rust train because Rust people has conjecture ? I ask the opposite question. What would happen if the only programming language left is C? Wouldn't we become better programmers and raise the bar so high…

> What would happen if the only programming language left is C? Wouldn't we become better programmers and raise the bar so high that the bug count drops to 0?

Is this a rhetorical question? Clearly the answer is no.

Re: ZZ is a modern formally provable dialect of C

#136

Post by MaxBarraclough »

a3p wrote: post #129
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…

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.

Re: ZZ is a modern formally provable dialect of C

#137

Post by iainmerrick »

rezeroed wrote: post #25
simias wrote: post #11

So it's more like a C transpiler than a dialect of C IMO (it effectively looks more Rust-like than C-like). I'm not just saying that for nitpicking the obviously vague definition of "dialect" but rather because it's a very important feature IMO, and actually makes this project potentially more useful to me. I'd be very wary of switching my toolchain to an experimental one in production, especially if I'm targeting so…

It will always emit C into a C compiler which will then emit the binary. Presumably we can dump the C before compilation?

Why?

For this purpose, C is a very convenient and very portable assembly language. You could use a verified C compiler like CompCert to convert it to machine code.

In an ideal world, there’d be no C compiler in the loop at all, sure. But in practice it’s not causing any trouble at all in a ZZ -> C -> machine code workflow. Quite the reverse, targeting C has some major benefits. (There are C compilers that are very fast, very highly optimizing, very portable, and/or verifiably correct.)

Edit to add: just realised I might have totally misunderstood your comment, sorry! Apologies for jumping the gun if so.

If you just mean can we save the generated C to disk instead of compiling it, yes, I would hope so too.

Re: ZZ is a modern formally provable dialect of C

#138

Post by iainmerrick »

mr_vile wrote: post #8

Okay, it's provable... what value do really get out of it? isn't the whole reason why we still use C because it gets so close to resolving (or at least acknowledging) hardware or platform-level implementation problems? we can continue to re-invent the language in isolation but you can't replace a hardware-level programming language in this manner.

It is surprising that the syntax is so different for a “dialect” of C, but apart from that --

If the semantics are very close to C, so you can do basically all the same stuff, but you also get guarantees that your code will absolutely never hit any undefined behavior, that’s great and tremendously useful. It absolutely could replace C in applications where C is still the most useful and practical language.

It would resolve a couple of major headaches in existing C code: security bugs caused by memory overflows (caused by using arrays or pointers in undefined ways); and highly optimizing compilers doing weird things to your code, by exploiting undefined edge cases.

If I know my code will definitely not hit any undefined behavior, that gives me a ton more confidence that it won’t have stupid buffer overflow bugs and I won’t get mysterious errors on certain platforms.

Re: ZZ is a modern formally provable dialect of C

#139

Post by loeg »

a3p wrote: post #126
loeg wrote: post #117

Earlier quoted context omitted.

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!

Re: ZZ is a modern formally provable dialect of C

#140

Post by a3p »

iainmerrick wrote: post #137
rezeroed wrote: post #25

Earlier quoted context omitted.

It will always emit C into a C compiler which will then emit the binary. Presumably we can dump the C before compilation?

Why? For this purpose, C is a very convenient and very portable assembly language. You could use a verified C compiler like CompCert to convert it to machine code. In an ideal world, there’d be no C compiler in the loop at all, sure. But in practice it’s not causing any trouble at all in a ZZ -> C -> machine code workflow. Quite the reverse, targeting C has some major benefits. (There are C compilers that are very fa…

Absolutely! The zz export command just dumps the C and SMT code along with makefiles for common build systems and stops there. Very handy for using it within other toolchains.
Post reply on HN