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

31–40 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#31

Post by scoutt »

oblio wrote: post #29
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…

The answer is size, power consumption and most of all, price.

I know I can do a wrist watch with a Raspberry Pi, but will it be profitable/convenient?

Re: ZZ is a modern formally provable dialect of C

#32

Post by firebacon »

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…

> 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 adding two numbers.

In my experience, panics in rust have been a major source of pain. In contrast to an exception, which you can catch, a panic behaves more like an abort. At least it has been that way in the past. Now, with a lot of libraries using panics to signalize runtime errors, coding in rust has at some times felt like I was using a bunch of badly written C libraries that internally call "abort()" and kill the process when something goes wrong that would have been totally handle-able without killing the whole process. That's the benefit of using a safe language, right?

I think lately the rust "community" has become aware of this issue and IMO the way things are going is that that panics, as they are designed, should basically not be used. But, without proper exceptions, that brings you back to the situation where an operation as trivial as adding two numbers either produces a return code that must be explicitly checked or may silently fail and produce an "undefined" result in some cases.

Re: ZZ is a modern formally provable dialect of C

#33

Post by dx87 »

scoutt wrote: post #27
dmos62 wrote: post #20

Earlier 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.

Yet we still see security issues in all of those. I'm not saying that everything should be re-written in a different language, but C developers saying "I'm a good developer, all those safety mechanisms would hold me back" doesn't hold water considering all the security vulnerabilities we see that would have been prevented if they had used a language with better safeguards.

Re: ZZ is a modern formally provable dialect of C

#34

Post by Nursie »

pjc50 wrote: 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…

There's the third sort of allocation that's often used in embedded systems - preallocated buffers, which are neither stack nor heap but set up by the .bss section of the executable.

These allow you to have very predictable memory usage.

Re: ZZ is a modern formally provable dialect of C

#35

Post by pjmlp »

pjc50 wrote: 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…

Unless it has changed, SPARK also forbids dynamic allocation.

Re: ZZ is a modern formally provable dialect of C

#36

Post by scoutt »

nicoburns wrote: post #28
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.

With years you get to put together a swiss-army toolset of libraries to deal with all that (like arrays, strings, etc.).

You know how they work, how far you can push them, the overhead, and all.

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 know it's reinventing the wheel, but I am sure that there are known simple libraries out there one can use. I use mine.

What I would like is a better precompiler, like assigning dynamic values to constants. But I won't change the language for that.

Re: ZZ is a modern formally provable dialect of C

#37

Post by scoutt »

dx87 wrote: post #33
scoutt wrote: post #27

Earlier quoted context omitted.

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. Yet we still see security issues in all of those. I'm not saying that everything should be re-written in a different language, but C developers saying "I'm a good developer, all those safety mechanisms would hold me back" doesn't hold water considering all the security vulnerabilities we see that would have been prevented if they had used a language w…

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

Re: ZZ is a modern formally provable dialect of C

#38

Post by oblio »

scoutt wrote: post #31
oblio wrote: post #29

Earlier quoted context omitted.

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…

The answer is size, power consumption and most of all, price. I know I can do a wrist watch with a Raspberry Pi, but will it be profitable/convenient?

Well, let's say I take the Intel P54 (https://en.wikipedia.org/wiki/List_of_Intel_microprocessors#...) as an example.

So basically an Intel Pentium from 1994, so from 26 (!) years ago. Size: 90 mm2, maximum power consumption: 10W, price at launch: $699.

Buuuut: production process 600nm.

Today every Intel CPU uses a 14nm production process, but let's go for a cheaper option and "use" the 22nm.

So the gate size is ~30x smaller today. And I know that the relation between the gate size and the die size is not linear (2x smaller gate size usually leads to a die size which is smaller by more than 2x), but let's go with the 30x, to keep things simple.

For the power I have no idea, but I'd assume that the power consumption would go down at least 30x.

Price: hard to say, but considering how hardware evolves, definitely more than 30x cheaper :-)

So a Intel Pentium with modern technology could look something like this:

Size: 3mm2 (probably less), maximum power consumption: 0.3W (probably way less), price at launch: $30 (I'd argue that it would be closer to 0.3$ :-) ).

I could be way off in the weeds here...

My guess is that it's just a matter of existing tooling, expertise, human resistance to change, companies wanting to a) not risk anything and b) to nickel and dime everything.

I'm arguing for an x86 because that way you could throw any kind of modern tooling at it. ARM or MIPS would probably be better candidates.

Re: ZZ is a modern formally provable dialect of C

#40

Post by pjmlp »

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.

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.

Post reply on HN