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

21–30 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#21

Post by dmos62 »

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…

I've not looked at ZZ yet, but when we talk about formal proofs, we're usually proving much more interesting properties than what a type system typically proves.

Re: ZZ is a modern formally provable dialect of C

#22

Post by pjc50 »

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 inconvenient. On the other hand, "MISRA C:2004, 20.4 - Dynamic heap memory allocation shall not be used."

Re: ZZ is a modern formally provable dialect of C

#23

Post by pjc50 »

dmos62 wrote: post #20
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.

I think most users are going to wait until CMSIS or their local equivalent is available: https://github.com/ARM-software/CMSIS_5

Besides, it's a big retraining effort.

Re: ZZ is a modern formally provable dialect of C

#24

Post by MrBuddyCasino »

dmos62 wrote: post #20
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.

Its slowly getting there, but no, right now there is a very limited number of target platforms that are supported, and the ecosystem is still very small and immature. You have to remember that there is a huge number of microcontrollers out there, with exotic architectures you have never heard of, and that LLVM definitely doesn't support. I'm not sure embedded Rust would even meaningfully exist without the work of Jorge Aparicio.

Re: ZZ is a modern formally provable dialect of C

#25

Post by rezeroed »

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…

It will always emit C into a C compiler which will then emit the binary.

Presumably we can dump the C before compilation?

Re: ZZ is a modern formally provable dialect of C

#27

Post by scoutt »

dmos62 wrote: post #20
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.

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 happens, I'll debug it. That's it. I'm not afraid of UB or dealing with pointers, even if there are 10K Rust users trying to FUD me. I know what I'm doing. Every embedded/kernel/driver developer know what they are doing. When shit happens, that's it, no big deal. You plug your debugger and solve the issue. It's not a nightmare that chases us in the middle of the day.

FUD alone is not enough for switching. So, why should I start thinking that a variable cannot change, because it's a constant (wasn't it a variable?), unless it can mutate, so it's a constant variable that can change because now is mutable?

Or constrain myself into borrow-checker torture for a thing I can do in a couple of instructions?

WHY?

2) This is not about a language problem, is about solving a programmer problem with language. If C = math, then you cannot do math simpler/better because today's mathematicians are sloppier. Or because bosses pressures people to deliver crappy products.

I'm not a genius. I'm far from it, and if any seasoned C programmer challenges me I'll probably run away. But embedded/kernel/driver development is harsh, so if a developer thinks that he/she cannot make it because language, then it's mostly about searching for an excuse. Time to change jobs.

The key is to think that a lot of people did (and does) a lot with so much less, for 40 years now. It's not a language problem. People have to learn to deal with it.

I was there too 20 years ago, when every C++ developer was afraid that they would lose their jobs because C#. It never happened. C++ is still one of the most used languages.

3) In my case, there are official libraries from manufacturers you have to use. Sometimes receiving customer support depends on if and how you use those libraries. All those libraries are in C. All the support is in C. All the examples are in C.

Yes, I know there is that engineer that has a Github repo with a library that works fine with that STM32 for that specific language, that now is getting support for embedded so in 5 years we could maybe put something in production. But, not for now.

Sorry for the length. Edited some typos.

Re: ZZ is a modern formally provable dialect of C

#28

Post by nicoburns »

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.

> but it's still a pleasure for me to write and have to deal with C

But wouldn't you love a C with things like first class support for arrays and support for namespaces / modules, etc.

Re: ZZ is a modern formally provable dialect of C

#29

Post by oblio »

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.

I hope that with IoT we get some commoditization and standardization in this space. Though ARM doesn't give me much hope. I don't get why there couldn't be 1-2-3-5 standard architectures and 10-20-50-100 hardware configurations that cover the full spectrum of embedded configurations.

We've had 32 bit x86 CPUs since 1985, surely we could produce a 100Mhz one for cheap enough that nobody would need to use 8 bit ones in 2020? I know that I'm just daydreaming and companies are stingy...

Post reply on HN