Live data from Hacker News

ZZ is a modern formally provable dialect of C

github.com

111–120 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#111

Earlier quoted context omitted.

Does Oberon have any major commerical usage? I read up on it a while back and thought it was a neat experiment

It doesn't that I know of. Relevant to the C space, there is an embedded platform for it: https://astrobe.com/Oberon.htm

One should note that this company is in business for around 20 years now, so they get by, even if they aren't SV like rich.

Re: ZZ is a modern formally provable dialect of C

#112
post #40
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.

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.

Re: ZZ is a modern formally provable dialect of C

#113

One question that isn’t obvious from the overview: This language compiles to C and asserts that your program will never exhibit undefined behavior; have they proved that ZZ is correct , ie that it will definitely never output C code that exhibits undefined behavior? If you really care about correctness, that seems important. I absolutely love the idea in general though.

It's always concerning to see a compiler not being written in the compiled language.

Re: ZZ is a modern formally provable dialect of C

#114
post #22

This is a great achievement in making formal methods accessible in pragmatic terms - something that actually works and can be used by normal humans. Would be nice to have an actual microcontroller example. > The standard library is fully stack based and heap allocation is strongly discouraged :/ - I can see why this is done, as it's hard, so banning it to make the problem tractable works. But it's also quite inconven…

the standard library does not allocate any heap memory, but heap modelling will be added to the prover eventually.

note that there are convenience tools to deal with heap-free targets (microcontrollers) such as tail variants (statically enforced flexible arrays):

https://github.com/aep/zz#metaprogramming-or-templates-tail-...

Re: ZZ is a modern formally provable dialect of C

#115
Pre- and post-condition annotations (`where` and `model`, respectively) are great. It's nice to see those in a new language.

Syntactically, this seems more like a Rust dialect than a C dialect. The primary relation to C seems to be portability (transpiler) and integration (ABI). This is true of most C-transpiled languages, though.

It's certainly cute, and potentially useful if your program is small enough to be solved by a SAT solver. Ideally relatively quickly, or those compile times will be poor. I wonder how it deals with machine registers, which are often something you would be using in embedded C.

Re: ZZ is a modern formally provable dialect of C

#116

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?

Re: ZZ is a modern formally provable dialect of C

#117
post #109

Earlier quoted context omitted.

I agree that it is. Looking at the page, I can't see how far this goes. Was my earlier comment completely wrong? Does ZZ allow the programmer to express a formal specification, e.g. to verify a sort function? If so, their examples are selling their language very short.

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/

Re: ZZ is a modern formally provable dialect of C

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

This is entirely orthogonal to the fine article and basically just a statement of personal preference. Having preferences is fine, and sure, if you like C you can take umbrage at some of the more flowery characterizations in the README, but it's not really the point of the language. There are lots of neat ideas in TFA that would be interesting to discuss; no one is interested in litigating the fate of C on embedded for the Nth time.

Re: ZZ is a modern formally provable dialect of C

#119

Earlier quoted context omitted.

>Do I really know how much cycles/stack it takes to do std::sort(a.begin(), a.end()); in that specific platform? No, so I cannot trust it. I also don't know how many cycles it takes for my implementation of quicksort apart from checking the output of a specific compiler and counting instructions. C is not, was not and will never be a portable assembler.

> I also don't know how many cycles it takes for my implementation of quicksort apart from checking the output of a specific compiler and counting instructions. On any modern out-of-order CPU, that doesn't get you close to determining the dynamic performance. Even with full knowledge of private microarchitectural details, you'd still have a hard time due to branch prediction.

The embedded/micro space is not out-of-order, broadly. Memory access latency may be variable, or not, but I would charitably assume OP knows their subject material and is either using cycles as a metaphor, or actually works with tiny hardware that has predictable memory access latency.

Re: ZZ is a modern formally provable dialect of C

#120
post #56

Earlier quoted context omitted.

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.

I know people often refer to C as portable assembly, but really it's not. That sounds like the sort of thing gets repeated by people who neither know C nor assembly. C is incomparably higher level than assembly and lacks the quirkiness modern instruction sets have which are focused on specific odd things modern processors do well.

I refer you to MASM macros in the late 1990s.

If you want the same runtime environment of asm without the tediousness of asm development, and a reasonable optimizer to save you more tediousness, you end up at C. I count that as close enough.

Post reply on HN