ZZ is a modern formally provable dialect of C
1–10 of 157 posts
Re: ZZ is a modern formally provable dialect of C
#2I though this would be more like Frama-C, in this spirit it doesn't look like C to me.
So not sure about possible adoption among C devs, even when the idea looks quite good.
Re: ZZ is a modern formally provable dialect of C
#3It can’t be a dialect of a language if the compiler of said language doesn’t compile it.
Re: ZZ is a modern formally provable dialect of C
#4It can’t be a dialect of a language if the compiler of said language doesn’t compile it.
https://en.wikipedia.org/wiki/Programming_language#Dialects,...
Plenty of well-known dialects are not subsets of said language (/compiled by its compiler).
Re: ZZ is a modern formally provable dialect of C
#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.
Re: ZZ is a modern formally provable dialect of C
#6Very 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 complicated. This may be a happy inbetween.
Re: ZZ is a modern formally provable dialect of C
#7I 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?
Re: ZZ is a modern formally provable dialect of C
#8Okay, 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.
Re: ZZ is a modern formally provable dialect of C
#9> 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.
[deleted]
Re: ZZ is a modern formally provable dialect of C
#10I 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?
"Beware of bugs in the above code; I have only proved it correct, not tried it."