Hacker News Reader

Comment by bsdpufferfish | Hacker News Reader

Competing languages don’t have spec, so their entire operation is unspecified. If they wrote it down then they would also have UB.

View on HN

By corollary does that mean that if there isn't a formal proof of how C compiles to assembly, and how those opcodes are interpreted by a particular CPU model, that C formally isn't specified to have any meaning to a CPU?

There is a formal proof if you use the CompCert C compiler:

https://compcert.org/

That would get you to the assembly generated, but not the behavior of the CPU in the question, which goes to show it's a pretty silly position to hold.

There are formally verified CPUs, they're just not the lovely high performance ones you probably want.

For what it's worth, this is a common sentiment people have when they first come to blows with formal. "If you can't verify everything, why verify anything?" is a reasonable question to ask but it's not a practical position to hold since formal does increase the quality of software/hardware. Don't argue for less formal, fight for more!

As a Rust fan, it sounds remarkably similar to "if you still need unsafe somewhere, why bother trying to limit unsafe at all"

Yes the CPU is vendor defined behavior. However they usually write a spec.

The point is “undefined behavior” is more about gaps in the standard than bugs in programs.

Undefined Behaviour in C is the opposite of a gap in the standard. It's behaviour that's addressed in the standard that for historic, political, and performance reasons is allowed to be inconsistent. That's the reason it sucks to have been bitten by it (e.g. to find out that shifting N-1 bits out of an N sized integer gives you 0 bits, but shift that Nth bit and all bets are off)

So your claim is that a new language could define a spec to a degree that it would not have similar problems?

Yes? The combination of "historic, political, and performance" is a particular choice. Our attitudes to all of these are different to when C was maturing, particularly where reliability and security are involved.

And not least of all, we've learned more about programming language development than when C was created.

Reply on news.ycombinator.com