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

11–20 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#11

Post by simias »

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 some niche DSP. On the other hand generating C and then compiling it as usual seems less of a hurdle to me. They actually point that out in the intro but I thought it might be worth mentioning it here.

Now I just quickly skimmed the readme but do they explain how they deal with interfacing with standard, non-ZZ C code? I assume they need some sort of "FFI" bindings like Rust to make the code safe.

Re: ZZ is a modern formally provable dialect of C

#12

Post by simias »

socialdemocrat wrote: post #6

Very cool idea! What I love about C is that all sorts of programming language can talk to its ABI and that it fits well with low level programming. However it is a cumbersome and unsafe language. This seems like a very nice solution. You can write in a much safer language while producing C code which does not look too alien relative to what you wrote I have been interested in Rust but thinking it looks a tad too comp…

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 prove to the language that the access is correct.

Re: ZZ is a modern formally provable dialect of C

#13

Post by wuschel »

socialdemocrat wrote: post #6

Very cool idea! What I love about C is that all sorts of programming language can talk to its ABI and that it fits well with low level programming. However it is a cumbersome and unsafe language. This seems like a very nice solution. You can write in a much safer language while producing C code which does not look too alien relative to what you wrote I have been interested in Rust but thinking it looks a tad too comp…

If you like this, it might be worth looking at ATS: http://www.ats-lang.org/

Re: ZZ is a modern formally provable dialect of C

#14

Post by speps »

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…

I think I found some FFI examples:

- Using ZZ struct in C: https://github.com/aep/zz/tree/master/tests/mustpass/inlinei...

- Using C code in ZZ: https://github.com/aep/zz/tree/master/tests/mustpass/ctype_i...

Re: ZZ is a modern formally provable dialect of C

#15

Post by lallysingh »

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.

Of course it isn't. It's portable (-ish) assembler. The only thing replacing C will be even more in the C spirit. Adding more checking in system-programming-friendly ways is the only way I can think of for improving the situation.

Re: ZZ is a modern formally provable dialect of C

#16

Post by fuklief »

Jaxan wrote: post #7

I like how they incorporate an SMT solver. They claim: “all code is proven”. What does that mean? What is proven about the code? Absence of memory bugs, or actual correctness of algorithms?

+1

What does it even mean that the language is formally provable ?!

Re: ZZ is a modern formally provable dialect of C

#18

Post by speps »

simias wrote: post #12
socialdemocrat wrote: post #6

Very cool idea! What I love about C is that all sorts of programming language can talk to its ABI and that it fits well with low level programming. However it is a cumbersome and unsafe language. This seems like a very nice solution. You can write in a much safer language while producing C code which does not look too alien relative to what you wrote I have been interested in Rust but thinking it looks a tad too comp…

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.

Re: ZZ is a modern formally provable dialect of C

#20

Post by dmos62 »

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.

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

Post reply on HN