> I just want compilers to treat UB the same as unspecified behavior, which cannot be assumed away.
Unspecified behavior is defined as the "use of an unspecified value, or other behavior where this International Standard provides two or more possibilities and imposes no further requirements on which is chosen in any instance".
Which (two or more) possibilities should the standard provide for out-of-bounds writes? Note that "do what the hardware does" wouldn't be a good specification because it would either (a) disable all optimizations or (b) be indistinguishable from undefined behavior.
I don't see any surprised compiler authors in that thread. The reporter immediately suggests the correct underlying reason for the bug and another compiler author even says that they wondered how long it would take for someone to notice this.
Even if you read any surprise into their messages they wouldn't be surprised that C does something completely unreasonable, they would be surprised that LLVM does something unreasonable (by default).
No, it isn't. The CSU ran with nuclear revival as one of their campaign promises and there seems to be some support for it among the population but it's nowhere to be found in the coalition agreement between CDU/CSU and SPD. Söder (the leader of the CSU) already backpaddled as well.
Really the only possibility for a nuclear revival in Germany would be a coalition between the climate-change-downplaying CDU/CSU and the straight-up-climate-change-denying AfD and I doubt that would be good for Germany's fight against climate change.
Yes and those two reactors make up two thirds of all new nuclear reactors in the US in the last 29 years. There is no nuclear renaissance in the US and it really doesn't look like there will be one in the (near) future. Especially given how extremely badly the construction of those three reactors (and the two cancelled reactors) went.
We have 2 billion new watts of nuclear on the grid in the last few years, and more coming with uprates and massive demand from hyperscalers. The goal here isn't wind and solar. It's clean energy in general.
> We have 2 billion new watts of nuclear on the grid in the last few years
Because two nuclear reactors came online in the last two years (after massive delays and cost overruns). In the last 29 years the US built three new nuclear reactors (the construction of two more was cancelled). How many watts of nuclear were shut down in that time span?
> and more coming with uprates and massive demand from hyperscalers
I'll believe it when I see it.
> The goal here isn't wind and solar. It's clean energy in general.
I agree. I don't think nuclear is bad. I'm just describing what is happening in the US: Solar and wind are growing fast, nuclear is struggling.
> The question is: should compiler authors be able to do whatever they want? I argue that they should not.
My question is: I see so many C programmers bemoaning the fact that modern compilers exploit undefined behavior to the fullest extent. I almost never see those programmers actually writing a "reasonable"/"friendly"/"boring" C compiler. Why is no one willing to put their ~money~ time where their mouth is?
> I almost never see those programmers actually writing a "reasonable"/"friendly"/"boring" C compiler. Why is no one willing to put their ~money~ time where their mouth is?
Because it is not much harder to simply write a new language and you can discard all the baggage? Lots of verbiage gets spilled about undefined behavior, but things like the preprocessor and lack of "slices" are way bigger faults of C.
Proebsting's Law posits that compiler optimizations double performance every 20 years. That means that you can implement the smallest handful of compiler optimizations in your new language and still be within a factor of 2 of the best compilers. And people are doing precisely that (see: Zig, Jai, Odin, etc.).
I'm willing to write a C compiler that detects all undefined behavior but instead of doing something sane like reporting it or disallowing it just adds the code to open a telnet shell with root privileges.
Can't wait to see the benchmarks.
I was thinking more along the lines of detectable instances with compiler introducing "optimizations", but as a C "programmer" I do not mind bounds checks and any other runtime improvements that stay true to the language.
If it's implementation-defined that you can turn them off when you're building for the PDP11, I'm sold.
Compilers already warn when they detect _unconditional_ undefined behavior. They just don't warn on _conditional_ undefined behavior because doing so would introduce far too many warnings.
Exploiting undefined behavior for optimization only requires local analysis, detecting whether that undefined behavior arises (either unconditionally or at all) requires global analysis. To put it differentially: The compiler often simply doesn't know whether the undefined behavior arises, it only knows that the optimization it introduces is valid anyway.
I was willing to, but the consensus was that people wouldn't use it.
C and C++ programmers complain about UB, but they don't really care.
TCC is probably the closest thing we have to that, and for me personally, I made all of my stuff build on it. I even did extra work to add a C99 (instead of C11) mode to make TCC work.
Shouldn't your blog post then condemn the C community at large for failing to use a more "reasonable" C compiler instead of complaining about compiler authors that "despite holding the minority world view, [...] have managed to force it on us by fiat because we have to use their compilers"?
You don't have to use their compilers. Most people do, because they either share this "minority" world view or don't care.
My blog post doesn't condemn the C community at large because it was the HN comments on that post where I found out that the C community is a bunch of hypocrites.
> spares you the trouble of navigating much of the zoo that is git cli design
Yeah. I understand the inner workings of git and am perfectly capable of using git on the command line but the git cli is just so horribly designed. I regularly have to google how to perform rather basic actions because the cli just isn't structured in any sensible way.
> In other words, how do we know that what we proof is still valid for the original code?
We don't. We will always have to trust _something_ (the hardware, the compiler, the specification, Coq's trusted kernel, ...). Formal verification is sadly often discussed as removing the possibility of bugs in their entirety. In practice, formal verification only makes bugs much less likey.
That said, yes, automatic translation between Rust and Coq massively reduces the complexity of the things you have to trust and should therefore be preferred over manual translation.
Every tool can only guarantee absence of some categories of bugs.
The most common ones, business logic, often escape verification simply because of wrong assumptions.
Simple example: some websites use the browser's default language to set your locale, some use your ip. Thus I travel to Poland and suddenly YouTube shows me Polish content and ads (this can be changed often, but not always, see Google docs idiocy). They will all unavoidably lead to business logic bugs because the assumptions are wrong in the first place.
That's why some industries have separate "verification" and validation" (V&V) activities.
Verification is checking against formal or at least known requirements like those being discussed in this thread.
Validation is a set of processes for ensuring the specifications actually correspond to how the product ought to work. "How it ought to work" is open-ended and meant to include real-world aspects you didn't know beforehand. For example business logic assumptions. But despite being open-ended it is possible to formalise and track the process of looking for issues systematically.
In your example of YouTube showing Polish content when you travel, verification is the process of checking the website uses the IP correctly because using the IP is specified somewhere, but validation is the process of asking "what's the right thing to do when a user travels, is it really to use the IP?" and "let's systematically research what issues are affecting users due to incorrect specifications that we should change".
The media is picking up any Boeing related incident and it is ignoring other incidents. Most of the incidents I read about in the last weeks had nothing at all to do with Boeing as a company.
Unspecified behavior is defined as the "use of an unspecified value, or other behavior where this International Standard provides two or more possibilities and imposes no further requirements on which is chosen in any instance".
Which (two or more) possibilities should the standard provide for out-of-bounds writes? Note that "do what the hardware does" wouldn't be a good specification because it would either (a) disable all optimizations or (b) be indistinguishable from undefined behavior.
reply