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

61–70 of 157 posts

Re: ZZ is a modern formally provable dialect of C

#61

Post by whatshisface »

cwzwarich wrote: post #55
hurrrrrrrr wrote: post #49

Earlier quoted context omitted.

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

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.

Re: ZZ is a modern formally provable dialect of C

#62

Post by whatshisface »

scoutt wrote: post #58
hurrrrrrrr wrote: post #52

Earlier quoted context omitted.

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…

>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 programmers will slowly erode compared to their competition. At first only the people who are really interested in technology will switch, but eventually only the curmudgeons will be left, clinging to an ineffective technology and using bad justifications to convince themselves they aren't handicapped. Is Rust the thing that everyone except the curmudgeons will eventually switch to? Who knows, but if you don't want to end up behind the industry then it might pay to try it out in production to see for yourself. If you don't make room for research and its attendant risks you will inevitably fall behind.

Re: ZZ is a modern formally provable dialect of C

#63

Post by Psyladine »

wheels wrote: post #56
lallysingh wrote: post #15

Earlier quoted context omitted.

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.

Bit like chicken & egg though, with processors chasing better implementations of C rather than better implementations of assembly:

https://queue.acm.org/detail.cfm?id=3212479

Re: ZZ is a modern formally provable dialect of C

#64

Post by uxp100 »

MrBuddyCasino wrote: post #24
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.

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

Yeah. Even on the best supported platforms it is very immature. If you want to use embedded rust you kinda have to let language drive your choice of platform, which isn’t ideal.

I wouldn’t use it at work yet, but it’s coming along.

Re: ZZ is a modern formally provable dialect of C

#65

Post by baq »

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…

A language is a tool and if you're saying the problem is with people using the tool wrong, it's only half true. New tools are being invented to handle problems both old and new and discrediting them with what amounts to 'get off my lawn' is counter-productive. There are problems that are impractical to solve without tools designed for them and safe pointers are a great example. Yes, you'll hook up your debugger and yes, you'll fix the problem. I once fixed a dangling pointer problem after two 12h debugging sessions and while it felt great, I'd rather not do that again. I know there are people hunting these for months, so you could say I haven't seen anything yet, and I'll agree - but it's an argument in favor of better tools, not the other way around.

Re: ZZ is a modern formally provable dialect of C

#67

Post by throwaway17_17 »

wuschel wrote: post #13
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…

If you like this, it might be worth looking at ATS: http://www.ats-lang.org/

I'm a fan of ATS, really I am, but recommending ATS to someone who said Rust looks too complicated made me literally laugh out loud. Like I said, I like ATS and don't particularly care for Rust, but ATS is in no way less complicated that Rust. But I really do feel like the laugh I had is going to make my day better, so thanks.

Just a note: the above is not sarcasm

Re: ZZ is a modern formally provable dialect of C

#68

Post by Doingmything123 »

scoutt wrote: post #58
hurrrrrrrr wrote: post #52

Earlier quoted context omitted.

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…

Not a Rust programmer.

It seems like there is a big difference between a "mathematical certainty that certain bugs will not occur" if you play by the rules and just be a better programmer so that you don't write errors. Not that you won't have bugs in Rust but it seems like we should move towards having our tooling do more of the heavy lifting in ensuring correctness. I don't believe you will ever have the bug count drop to zero. I do believe in mathematical certainties though.

Re: ZZ is a modern formally provable dialect of C

#69

Post by jcranmer »

scoutt wrote: post #58
hurrrrrrrr wrote: post #52

Earlier quoted context omitted.

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…

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

Given that C was the dominant programming language for UNIX applications for over a decade, I think we can look to history for an answer to this question. And I believe the record shows that the answer is "no."

Re: ZZ is a modern formally provable dialect of C

#70

Post by non-entity »

pjmlp wrote: post #40
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.

Does Oberon have any major commerical usage? I read up on it a while back and thought it was a neat experiment
Post reply on HN