5 ms·

This article comes close to making a fallacious argument about formal methods, which is that formal methods aren't useful unless you can exactly specify how som

This article comes close to making a fallacious argument about formal methods, which is that formal methods aren't useful unless you can exactly specify how something works. I use model checking (a form of formal methods) daily. I separate the process into three domains: things that must be fully specified, things that can be fully specified, and things that, with the appropriate mitigation, need only have certain properties verified. Most software fits just fine in the latter category. Spend your time on fully verifying process isolation, cryptography, certain core runtime functions / behaviors, and logic relating to authentication and authorization. Everything else can be partially verified, which is much easier. Verify termination, no UB, memory safety, and that function contracts, data structure invariants, and API boundaries are followed. A PDF implementation, a web browser, or a random server application fits cleanly into this decomposition. It matters little if the PDF is rendered oddly, or if the web browser can't interpret a page. But, it matters greatly if these errors could result in a vulnerability that could be exploited, or to a lesser extent, if these errors resulted in the software crashing. Pure formal methods is academic. Apply engineering to this, and you get a real world and practical framework for making software safer.

dullcrisp 1mo ago
I’m not just being funny, but how do you define undefined behavior?
- antonvs 1mo 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 1mo 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 1mo 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 1mo 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 1mo 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.
DenisM 1mo ago
Do you find that given a formal spec an agent can write complete implementation you don’t have to even read? I keep thinking about various ways of “pushing back” on an agent, shortening feedback loop and extending what we can grantee about results. At the most low level we can nullify probability of the next token if that token is not desirable (eg json schema enforcement under constrained inference), this is the fastest pushback. Various compiler checks, linters, unit tests, exotic type systems, e2e tests, production traces. Wondering what else is out there. On a tangent, iirc pascal allowed single-pass compilation, so I wonder if we can embed compiler directly into inference, sort of constrained inference on steroids.
- nanolith 1mo ago
  I think that reading and reviewing software is responsible. Source code exists for humans to read first, and for computers to read second. Programming languages are unambiguous, and most languages take well to abstraction. Software can be written at a level that is appropriate for human review. Boilerplate can be avoided. It's well written when it is easy for stake holders to understand directly, without translation and without an LLM to summarize it. Software should be the output artifact of the process, because it exactly describes the behavior of the system. The formal specification explains how the software embodiment must work, and in constructive proofs, it's even possible to extract the software embodiment from this specification. But, from a practical perspective, this is too time consuming. Instead, specification should be written to explain the rules that software must follow, instead of the exact behavior. In this case, the source code is still an important artifact, and it should be reviewed and improved upon as part of the process.

dullcrisp 1mo ago

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

antonvs 1mo 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 1mo 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 1mo 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 1mo 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 1mo 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.

DenisM 1mo ago

Do you find that given a formal spec an agent can write complete implementation you don’t have to even read? I keep thinking about various ways of “pushing back” on an agent, shortening feedback loop and extending what we can grantee about results. At the most low level we can nullify probability of the next token if that token is not desirable (eg json schema enforcement under constrained inference), this is the fastest pushback. Various compiler checks, linters, unit tests, exotic type systems, e2e tests, production traces. Wondering what else is out there. On a tangent, iirc pascal allowed single-pass compilation, so I wonder if we can embed compiler directly into inference, sort of constrained inference on steroids.

nanolith 1mo ago
I think that reading and reviewing software is responsible. Source code exists for humans to read first, and for computers to read second. Programming languages are unambiguous, and most languages take well to abstraction. Software can be written at a level that is appropriate for human review. Boilerplate can be avoided. It's well written when it is easy for stake holders to understand directly, without translation and without an LLM to summarize it. Software should be the output artifact of the process, because it exactly describes the behavior of the system. The formal specification explains how the software embodiment must work, and in constructive proofs, it's even possible to extract the software embodiment from this specification. But, from a practical perspective, this is too time consuming. Instead, specification should be written to explain the rules that software must follow, instead of the exact behavior. In this case, the source code is still an important artifact, and it should be reviewed and improved upon as part of the process.