8 ms·

I’m not just being funny, but how do you define undefined behavior?

antonvs 15d ago
You can define what constitutes undefined behavior without defining the behavior itself. Programming language definitions rely on this. So “verifying no UB” means verifying that a program is not performing any operations that have undefined behavior. Simple example: dereferencing an uninitialized pointer.
- dullcrisp 15d ago
  I get that, but I meant more philosophically, why is it especially useful to verify that no behavior is undefined if the defined behavior is also not defined, other that according to the compiler spec?
  - antonvs 15d ago
    I may be missing what you're asking. To extend the example I gave, it's very useful to be able to verify that a program never dereferences an uninitialized pointer. In general, it's very useful to be able to verify that a program doesn't do anything that could cause UB.
    - dullcrisp 15d ago
      That’s fair I suppose I’m being a bit obtuse. But this level of formal verification gets you to the level of confidence you’d have if you had written the program in Rust or Java in the first place. The original post was talking about formally verifying what the system does as a whole, not just verifying the absence of a certain class of errors. I’m not questioning the value of eliminating null pointer dereferences that do exist, just the value of holding a formal proof of the absence of null pointer dereferences in a certain piece of code, given that there are many other possible bugs that that code could contain. I mean, if I had a formal proof that my banking system could never double-spend money, that could be a useful property that someone would want to know about the system. If I have a proof that my banking system never dereferences a null pointer, there’s not very much I can be sure of on the basis of such a proof.
      - nanolith 15d ago
        The difference is that Rust and Java can only verify certain properties. I can build model checks to verify any property that I can discharge with an SMT solver, which is significantly more powerful. For instance, I can build function contracts that verify that if a function succeeds, it performs certain actions, and if it fails, it does not. I can verify that a function properly manages external resources, performs authorization checks, or always follows data structure invariants. I don't need to build full formal specifications to do this. I can verify just the subset that is important. I can do more than what Rust or Java provides. I can add more rules that must be followed, or in cases where it doesn't matter, I can relax specific rules without reaching for clumsy annotations like "unsafe", or using an FFI.
        dullcrisp 15d ago
        Yeah again fair enough. You can use formal methods to provably maintain invariants that are useful to you in development without shipping formal proofs of full system behavior.

You can define what constitutes undefined behavior without defining the behavior itself. Programming language definitions rely on this. So “verifying no UB” means verifying that a program is not performing any operations that have undefined behavior. Simple example: dereferencing an uninitialized pointer.

dullcrisp 15d ago
I get that, but I meant more philosophically, why is it especially useful to verify that no behavior is undefined if the defined behavior is also not defined, other that according to the compiler spec?
- antonvs 15d ago
  I may be missing what you're asking. To extend the example I gave, it's very useful to be able to verify that a program never dereferences an uninitialized pointer. In general, it's very useful to be able to verify that a program doesn't do anything that could cause UB.
  - dullcrisp 15d ago
    That’s fair I suppose I’m being a bit obtuse. But this level of formal verification gets you to the level of confidence you’d have if you had written the program in Rust or Java in the first place. The original post was talking about formally verifying what the system does as a whole, not just verifying the absence of a certain class of errors. I’m not questioning the value of eliminating null pointer dereferences that do exist, just the value of holding a formal proof of the absence of null pointer dereferences in a certain piece of code, given that there are many other possible bugs that that code could contain. I mean, if I had a formal proof that my banking system could never double-spend money, that could be a useful property that someone would want to know about the system. If I have a proof that my banking system never dereferences a null pointer, there’s not very much I can be sure of on the basis of such a proof.
    - nanolith 15d ago
      The difference is that Rust and Java can only verify certain properties. I can build model checks to verify any property that I can discharge with an SMT solver, which is significantly more powerful. For instance, I can build function contracts that verify that if a function succeeds, it performs certain actions, and if it fails, it does not. I can verify that a function properly manages external resources, performs authorization checks, or always follows data structure invariants. I don't need to build full formal specifications to do this. I can verify just the subset that is important. I can do more than what Rust or Java provides. I can add more rules that must be followed, or in cases where it doesn't matter, I can relax specific rules without reaching for clumsy annotations like "unsafe", or using an FFI.
      - dullcrisp 15d ago
        Yeah again fair enough. You can use formal methods to provably maintain invariants that are useful to you in development without shipping formal proofs of full system behavior.