7 ms·

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 progr

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.

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.