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
ZZ is a modern formally provable dialect of C
111–120 of 157 posts
Re: ZZ is a modern formally provable dialect of C
#112> 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.
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
#113One 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.
Re: ZZ is a modern formally provable dialect of C
#114This 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…
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
#115Syntactically, 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
#116I 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…
Re: ZZ is a modern formally provable dialect of C
#117Earlier 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…
Re: ZZ is a modern formally provable dialect of C
#118> 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
#119Earlier 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.
Re: ZZ is a modern formally provable dialect of C
#120Earlier 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.
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.