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

81–90 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#81

Post by AstralStorm »

oblio wrote: post #48
scoutt wrote: post #45

Earlier quoted context omitted.

Then you need external RAM, storage, a video card or companion chip for a display, a chip for holding the BIOS and a power supply (if not many) for all that. x86 as is, is not good enough for my wrist watch. You can use a small ARM with integrated flash, RAM and LCD controller. Does it need MMU for Linux? There is family of products for that. Or use another family for bare-metal systems. You can see how the thing sta…

Well, I just used the Pentium example because it was easy to source the data :-) But my main point was to dump super old and limited architectures when these days we can economically use modern architectures we use everywhere else (x86/ARM/MIPS, whatever). If we wanted to, we could literally hoist designs from 20+ years ago and use newer production technologies to make them embeddable. Using mainstream tech stacks is…

Hoisting old designs is unnecessary when you have x86 processors like Intel Atom, which are exactly that, and all the versions of ARM Cortex-R3 and R0.

The problem is not the processor, it's the lack of MMU and/or special DMA or interrupt engines and special GPIO. No kernel is potentially ported to such custom infrastructure, and if you have a very tiny flash, few of the ones which could will fit. (Say, target L4, porting Fiasco or OKL4.)

Re: ZZ is a modern formally provable dialect of C

#82

Post by whatshisface »

scoutt wrote: post #72
whatshisface wrote: post #62

Earlier quoted context omitted.

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

Not exactly, I'm saying that if you stay behind and don't adopt something, where that something is whatever the industry switches to after C, you will eventually be left behind. Of course it is also possible (and likely for many people) to die or retire before that happens. It's not like C is going away any time soon.

Re: ZZ is a modern formally provable dialect of C

#83

Post by lwb »

MaxBarraclough wrote: post #79

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…

Seems like they are using a narrow definition of "mathematically provable" -- they only thing that appears to be proven is that "all memory access is mathematically proven to be defined". Which just seems like a fancy way of achieving the same thing as a type checker? Either way, cool project, but is there anything else that ZZ can prove?

Re: ZZ is a modern formally provable dialect of C

#84

Post by michaelt »

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.

C's strength is the ecosystem:

* Your microprocessor has a C compiler and standard library, as does every processor you might ever switch to. All the hardware documentation that isn't tables in a PDF will be in C.

* Your target's static analysis tools and interactive debuggers will all support C.

* Every RTOS and embedded library/filesystem/whatever will support (and likely be written in) C.

* All experienced embedded developers are fluent in C.

* Nobody ever got fired for choosing C for an embedded project.

The disadvantages of C are many and well known.

Re: ZZ is a modern formally provable dialect of C

#85

Post by nickpsecurity »

non-entity wrote: post #70
pjmlp wrote: post #40

Earlier quoted context omitted.

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.

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

Re: ZZ is a modern formally provable dialect of C

#86

Post by oblio »

AstralStorm wrote: post #81
oblio wrote: post #48

Earlier quoted context omitted.

Well, I just used the Pentium example because it was easy to source the data :-) But my main point was to dump super old and limited architectures when these days we can economically use modern architectures we use everywhere else (x86/ARM/MIPS, whatever). If we wanted to, we could literally hoist designs from 20+ years ago and use newer production technologies to make them embeddable. Using mainstream tech stacks is…

Hoisting old designs is unnecessary when you have x86 processors like Intel Atom, which are exactly that, and all the versions of ARM Cortex-R3 and R0. The problem is not the processor, it's the lack of MMU and/or special DMA or interrupt engines and special GPIO. No kernel is potentially ported to such custom infrastructure, and if you have a very tiny flash, few of the ones which could will fit. (Say, target L4, po…

Ok, but that doesn't mean that such designs couldn't be made and then standardized, right?

Re: ZZ is a modern formally provable dialect of C

#87

Post by marta_morena »

This is just another symptom of why OpenSource often sucks. Instead of somehow coordinating and focusing their efforts, everyone seems to need to start their own spin off "inspired" by other projects.

When do people realize that building a new language is almost always going to fail and only very very few languages ever reach anything close to adoption.

Instead of spending all this time writing your own doomed language, why not try to contribute to a project like LLVM or Rust and add your provable subset there?

The same goes for Linux, which is the paradigm of wasted efforts.

Re: ZZ is a modern formally provable dialect of C

#88

Post by augusto-moura »

lwb wrote: post #83
MaxBarraclough wrote: post #79

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…

Seems like they are using a narrow definition of "mathematically provable" -- they only thing that appears to be proven is that "all memory access is mathematically proven to be defined". Which just seems like a fancy way of achieving the same thing as a type checker? Either way, cool project, but is there anything else that ZZ can prove?

In the README there's a example of proving a simple state machine open > read > close [1]

Just read the docs™

[1] https://github.com/aep/zz#theory

Re: ZZ is a modern formally provable dialect of C

#89

Post by jdc »

scoutt wrote: post #36
nicoburns wrote: post #28

Earlier quoted context omitted.

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

Doesn't C model the PDP-11 more so than ARM or x86?

Re: ZZ is a modern formally provable dialect of C

#90

Post by lwb »

augusto-moura wrote: post #88
lwb wrote: post #83

Earlier quoted context omitted.

Seems like they are using a narrow definition of "mathematically provable" -- they only thing that appears to be proven is that "all memory access is mathematically proven to be defined". Which just seems like a fancy way of achieving the same thing as a type checker? Either way, cool project, but is there anything else that ZZ can prove?

In the README there's a example of proving a simple state machine open > read > close [1] Just read the docs™ [1] https://github.com/aep/zz#theory

Ah ok, not sure how I missed that. That still seems to be within the realm of a type system, no? Or would you consider type systems a subset of mathematically provable systems?
Post reply on HN