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

51–60 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#51

Post by [deleted] »

hurrrrrrrr wrote: post #49
scoutt wrote: post #36

Earlier quoted context omitted.

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…

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

[deleted]

Re: ZZ is a modern formally provable dialect of C

#52

Post by hurrrrrrrr »

scoutt wrote: post #37
dx87 wrote: post #33

Earlier quoted context omitted.

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

But if we get rid of a whole class of bugs and vulnerabilities, the number of bugs will go down, no?

Re: ZZ is a modern formally provable dialect of C

#54

Post by pjc50 »

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…

People have more or less converged on ARM for large things and 8051 for tiny things. I suspect the remainder are hiding in culturally isolated niches; I don't really know why people are still targeting PIC16, for example.

There's also the DSP subset where people need to write inner loops in highly platform-specific assembler. e.g. my employer Cirrus has our own "Coyote" architecture for which we have a C compiler: https://statics.cirrus.com/pubs/proDatasheet/CS4970x4_F1.pdf

"Cheap" isn't just about BOM price, the power consumption matters too.

Re: ZZ is a modern formally provable dialect of C

#55

Post by cwzwarich »

hurrrrrrrr wrote: post #49
scoutt wrote: post #36

Earlier quoted context omitted.

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…

>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

#56

Post by wheels »

lallysingh wrote: post #15
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.

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.

Re: ZZ is a modern formally provable dialect of C

#57

Post by Cyph0n »

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’m a C developer working in the SP routing space.

Personally, I do not enjoy debugging memory corruption issues. I especially would not enjoy doing this under customer pressure...

Of course, in some spaces, C is basically the only option. But when you have options, and you’re working with a large enough codebase, C is a terrible choice.

Re: ZZ is a modern formally provable dialect of C

#58

Post by scoutt »

hurrrrrrrr wrote: post #52
scoutt wrote: post #37

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

But if we get rid of a whole class of bugs and vulnerabilities, the number of bugs will go down, no?

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 that the bug count drops to 0?

Re: ZZ is a modern formally provable dialect of C

#59

Post by gonzus »

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.

I would. I am keeping an eye on the zig programming language, exactly because of these reasons: https://ziglang.org/

Re: ZZ is a modern formally provable dialect of C

#60

Post by steveklabnik »

firebacon wrote: post #32
simias wrote: post #12

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

What libraries are using panics for runtime errors?
Post reply on HN