6 ms·

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

dwattttt 3y ago
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?
- ryao 3y ago
  There is a formal proof if you use the CompCert C compiler: https://compcert.org/ https://compcert.org/
  - dwattttt 3y ago
    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.
- sweetjuly 3y ago
  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!
  - dwattttt 3y ago
    As a Rust fan, it sounds remarkably similar to "if you still need unsafe somewhere, why bother trying to limit unsafe at all"
- bsdpufferfish 3y ago
  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.
  - dwattttt 3y ago
    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)
    - bsdpufferfish 3y ago
      So your claim is that a new language could define a spec to a degree that it would not have similar problems?
      - dwattttt 3y ago
        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.

dwattttt 3y ago

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?

ryao 3y ago
There is a formal proof if you use the CompCert C compiler: https://compcert.org/ https://compcert.org/
- dwattttt 3y ago
  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.
sweetjuly 3y ago
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!
- dwattttt 3y ago
  As a Rust fan, it sounds remarkably similar to "if you still need unsafe somewhere, why bother trying to limit unsafe at all"
bsdpufferfish 3y ago
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.
- dwattttt 3y ago
  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)
  - bsdpufferfish 3y ago
    So your claim is that a new language could define a spec to a degree that it would not have similar problems?
    - dwattttt 3y ago
      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.