I love this idea. Does anyone know what the compile-time performance is like?
ZZ is a modern formally provable dialect of C
71–80 of 157 posts
Re: ZZ is a modern formally provable dialect of C
#72Earlier quoted context omitted.
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…
> Should everybody drop C/C++/whatever and rush into the Rust train because Rust people has conjecture? The way these things usually work in practice, the evidence that a new paradigm improves things usually builds up slowly. There will never be a point at which someone proves mathematically that C is obsolete. Instead, the gentle advantages of other options will get stronger and stronger, and the effectiveness of C…
I'm sorry you see things in terms of competition and curmudgeons. But I see your point, it's just another type of FUD: don't stay behind and adopt Rust because you'll be a curmudgeon.
Re: ZZ is a modern formally provable dialect of C
#73Earlier quoted context omitted.
> 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.
My personal opinion, is basically for 3 reasons: 1) There is no need to. C already has all we need to build our systems. The rest is seen as overhead/over-complication. Regarding Rust, I try to keep up to date about its progress. Unfortunately most of the diseases that Rust cures are not much of a trouble in embedded. My last UB, memory leak of loose pointer happened years ago. It will happen again and when it happen…
"Every embedded/kernel/driver developer know what they are doing"
If that was true, then we wouldn't see more memory bugs found every time academics test a new analyzer or testing tool on open code programmed in C or C++. Microsoft said 70% of the problems they saw were memory safety. Linux has a ton of them. Even OpenBSD has many security fixes for memory safety. Your claim is mythical in the general case even if some individuals working on small codebases can pull it off.
https://www.zdnet.com/article/microsoft-70-percent-of-all-se...
https://events19.linuxfoundation.org/wp-content/uploads/2017...
Re: ZZ is a modern formally provable dialect of C
#74> 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.
Or anywhere else.
Lots of people don't enjoy using C for various reasons, but generally programmers don't get to choose what language they work in, they get paid to work in whatever language is needed.
Whether programmers like it or not for non personal projects doesn't actually matter too much. If you don't like using C, then don't take jobs programming in C. Just don't whine when that makes it more difficult to get a job.
Re: ZZ is a modern formally provable dialect of C
#75Earlier 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…
> operation will just panic at runtime if the array is too short Exactly, rust doesn't provide a good solution to this problem at all. Panics in rust are an escape hatch used to ensure the language stays "safe" in situations where the compiler can not prove a given behaviour at compile time, but where it would have made the language too ugly if you had to wire through Result types for all the trivial operations like…
A panic in Rust nicely captures the category of errors which the programmer asserts should be impossible, which generally cannot be recovered well from. A panic is kind of catchable, but it only works in the sense of killing only part of the process rather than the entire process (like abort does).
If errors are expected, then you should Result instead of a panic. If people are using panics instead of Result for these kinds of errors, then the library is wrong. I'm curious what examples you have where this is happening.
Re: ZZ is a modern formally provable dialect of C
#76Earlier quoted context omitted.
> Yet we still see security issues in all of those That's the typical excuse. That's the FUD I mentioned about. Bugs will keep existing and so security issues, no matter the language you use.
We need regulation to make companies liable for CVEs, then this will stop being FUD, easy.
It says something of our profession that we have all of our products come with a legal document that effectively says it's not our fault if the product doesn't do what it's supposed to do.
Re: ZZ is a modern formally provable dialect of C
#77> 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.
Or anywhere else. Lots of people don't enjoy using C for various reasons, but generally programmers don't get to choose what language they work in, they get paid to work in whatever language is needed. Whether programmers like it or not for non personal projects doesn't actually matter too much. If you don't like using C, then don't take jobs programming in C. Just don't whine when that makes it more difficult to get…
It does matter if the reasons why they do not like it are good.
Decision makers should listen to such input instead of deciding on programming language by fiat or convention. Including hardware choices. Of course this should be weighted by market availability and cost of both hardware and programmers.
Typically the reason C is used because there's no other toolchain available for said embedded device, except assembler, and they do not wish to invest in building or extending one. Those devices often do not have a kernel with POSIX-like syscalls to adapt an existing full blown libc, nor provide one.
Some embedded chipset libraries are also written in C sprinkled with copious assembly, so the language that's used with these has to be very easily interoperable.
Re: ZZ is a modern formally provable dialect of C
#78Earlier quoted context omitted.
> 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.
On most (small, I'm not talking about mini linux) embedded systems, instruction counting will tell you how long something takes to run. In fact, the compilers available are often so primitive that operation counting in the source code can sometimes tell you how long something will take.
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.
Re: ZZ is a modern formally provable dialect of C
#79I 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 new language which isn't C at all. Nothing wrong with that, but if I don't instantly recognise the syntax as C, I wouldn't call it a C dialect.
They also put formally provable dialect of C. Their language compiles to C code which is guaranteed to be free from undefined behaviour. This is not the same thing as a language where hard guarantees can be made about program behaviour, such as SPARK [2] or Dafny [3].
If the authors are reading this, I urge you to improve your project summary. Your language does not allow me to prove program correctness, instead it protects me from C's undefined behaviour. That's still a great idea! Please make this clear!
[0] https://news.ycombinator.com/item?id=22102658
[1] https://en.wikipedia.org/wiki/OpenCL#OpenCL_C_language
[2] https://en.wikipedia.org/wiki/SPARK_(programming_language)
Re: ZZ is a modern formally provable dialect of C
#80I 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?
That the code is provably free of C undefined behavior
Looking at the example code, [0] it's clear you're correct.
As I just rambled about in another comment in this thread, their project summary isn't clear about this. Still a great idea for a language though.
[0] https://github.com/aep/zz/tree/master/examples/hello/src