3 ms·

With LLMs revolutionising programming, maybe there's not much room left for using formal methods. Postmortem: The problem that needed solving: Computer program

With LLMs revolutionising programming, maybe there's not much room left for using formal methods. Postmortem: The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions. The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas. Problems they ignored: First, the problem they tried to solve wasn't the problem they were given -- this would be OK if the researchers produced usable methods on time. Second, if the formula is sufficiently detailed, it becomes effectively an executable program in its own right, and so you're back to square one. Thirdly, the formula might not capture a programmer's intent either. How they tried solving it: Spent 60 years not producing nearly any working product, except for final-year-projects done by their Bachelor's students. Published endless papers in conferences and journals*. Spent a few decades telling the software industry that it should drop everything and use formal methods. Assessment: Like a lot of software engineering fads that are promised as panaceas, this probably had a niche application somewhere, but its problems were ignored by its advocates and it underdelivered. * - Some of the theory they worked on was interesting in its own right: Type theory, constructive logic, computerised proof assistants, computable topology (and domain theory), substructural logics, some category theory, etc. I just think that now that LLMs are revolutionising programming, it's too late for this stuff to deliver anything to Software Engineering, and this stuff turned out to be of purely intellectual interest.

nanolith 3y ago
LLMs and other generative AI methods are nowhere near replacing the need for better reasoning about software, especially in safety critical systems.
- ogogmad 3y ago
  Maybe, but I'm not totally convinced: If an AI understands intentions, then it can carry out our intentions without us doing any traditional programming, specified using only plain English, especially in a safety-critical situation where this would probably be the best thing to do. Anyway, how would formal methods measurably help here [EDIT: By here, I mean security critical applications]? And have they shipped anything yet in that area, given that we've been waiting 60 years for them to do that? The answer is partially yes, admittedly, with TLA+. What else have they shipped?
  - nanolith 3y ago
    If, by "here", you mean AI, the answer is "unlikely". I was replying to the GP's assumption that such technology exists for traditional software. It does. CBMC exists today, and can be used to enforce function contracts in C, Java, and C++. Similar systems are being tested for Rust. Spark is a subset of Ada that incorporates function contract enforcement using a combination of model checking and a proof assistant. There are commercial projects using Spark today. seL4 was built from the ground up using Isabelle / HOL in order to formally verify their process isolation guarantees. There are much easier ways to do much of the work done in seL4 today. I use formal methods daily. About 95% of my work is checked using model checking. The rest is extracted to C using Lean 4.
    - ogogmad 3y ago
      I've heard of seL4, but I don't think it gets used much in the software industry. Not getting used kind of defeats the point of it, unless we need another 20 years for the formal methods people to produce an OS kernel people will actually use, while the AIs are eliminating programming as a field altogether. I'll need to think about the other stuff you said. I reserve a high level of skepticism to everything you've said.
      - nanolith 3y ago
        The existence of seL4 and its ability to be used in real projects certainly proves that formal methods has been effectively used to improve safety and security in shipping products, which was the question you asked if I understood it correctly... > while the AIs are eliminating programming as a field altogether. Where? So far, GPT-4 gets confused when given a specification with more than a dozen logic variables, and confidently regurgitates things that are, best case, partially working, and worst case, completely broken, based on a generative model trained on Stack Overflow and other forums. It's a cute concept, but it's closer to Eliza than eliminating this field. I can give it a logic problem that a freshman CS student can solve, and it will confidently give me the wrong answer. While I'm sure that LLMs will get better over time, I personally think their current application in software development has been over-hyped. There are plenty of papers, including the (in)famous "Stochastic Parrots" paper that are quite scathing. Based on my own tire kicking experience, I'm not convinced that LLMs can replace much more than boilerplate programming unless there are significant breakthroughs well beyond the current state of the art. Not incremental changes, but a complete reinvention of the current science. You can be skeptical regarding formal methods, but I use formal methods daily. It adds roughly 25% overhead over just unit testing to model check software, which easily covers 95% of the code base. The important parts -- enforcing function contracts, data flow, resource management, and correct usage patterns for things like cryptographic primitives -- are actually quite trivial to implement using an SMT solver. There is difficulty when dealing with loops, recursion, data structures, and algorithms, but most code out there can be abstracted away from these concepts. Contract enforcement at the library and framework level are certainly possible using tools as they exist today.
moritzwarhier 3y ago
> The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions. > The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas. The problem is documenting the intent of a rule-based system and confirming that it acts as expected. As every programmer knows, thoroughly defining intended behavior is the meat of impmenting said behavior. Often refining the intent based on thinking through or implementing intermediate solutions. This is not just because of the difficulty to make computers behave the way we want to, it includes the difficulty of defining how we want it to behave, too. There is no silver bullet that can remove ambiguity from human instructions, or always guess "correctly" when missing clear instructions. Because by definition, what is correct?

nanolith 3y ago

LLMs and other generative AI methods are nowhere near replacing the need for better reasoning about software, especially in safety critical systems.

ogogmad 3y ago
Maybe, but I'm not totally convinced: If an AI understands intentions, then it can carry out our intentions without us doing any traditional programming, specified using only plain English, especially in a safety-critical situation where this would probably be the best thing to do. Anyway, how would formal methods measurably help here [EDIT: By here, I mean security critical applications]? And have they shipped anything yet in that area, given that we've been waiting 60 years for them to do that? The answer is partially yes, admittedly, with TLA+. What else have they shipped?
- nanolith 3y ago
  If, by "here", you mean AI, the answer is "unlikely". I was replying to the GP's assumption that such technology exists for traditional software. It does. CBMC exists today, and can be used to enforce function contracts in C, Java, and C++. Similar systems are being tested for Rust. Spark is a subset of Ada that incorporates function contract enforcement using a combination of model checking and a proof assistant. There are commercial projects using Spark today. seL4 was built from the ground up using Isabelle / HOL in order to formally verify their process isolation guarantees. There are much easier ways to do much of the work done in seL4 today. I use formal methods daily. About 95% of my work is checked using model checking. The rest is extracted to C using Lean 4.
  - ogogmad 3y ago
    I've heard of seL4, but I don't think it gets used much in the software industry. Not getting used kind of defeats the point of it, unless we need another 20 years for the formal methods people to produce an OS kernel people will actually use, while the AIs are eliminating programming as a field altogether. I'll need to think about the other stuff you said. I reserve a high level of skepticism to everything you've said.
    - nanolith 3y ago
      The existence of seL4 and its ability to be used in real projects certainly proves that formal methods has been effectively used to improve safety and security in shipping products, which was the question you asked if I understood it correctly... > while the AIs are eliminating programming as a field altogether. Where? So far, GPT-4 gets confused when given a specification with more than a dozen logic variables, and confidently regurgitates things that are, best case, partially working, and worst case, completely broken, based on a generative model trained on Stack Overflow and other forums. It's a cute concept, but it's closer to Eliza than eliminating this field. I can give it a logic problem that a freshman CS student can solve, and it will confidently give me the wrong answer. While I'm sure that LLMs will get better over time, I personally think their current application in software development has been over-hyped. There are plenty of papers, including the (in)famous "Stochastic Parrots" paper that are quite scathing. Based on my own tire kicking experience, I'm not convinced that LLMs can replace much more than boilerplate programming unless there are significant breakthroughs well beyond the current state of the art. Not incremental changes, but a complete reinvention of the current science. You can be skeptical regarding formal methods, but I use formal methods daily. It adds roughly 25% overhead over just unit testing to model check software, which easily covers 95% of the code base. The important parts -- enforcing function contracts, data flow, resource management, and correct usage patterns for things like cryptographic primitives -- are actually quite trivial to implement using an SMT solver. There is difficulty when dealing with loops, recursion, data structures, and algorithms, but most code out there can be abstracted away from these concepts. Contract enforcement at the library and framework level are certainly possible using tools as they exist today.

moritzwarhier 3y ago

> The problem that needed solving: Computer programs make mistakes because they're too literal and they don't understand a programmer's intentions. > The problem they tried to solve instead: Computer programs make mistakes because we don't write out mathematical formulas detailing how programs should behave, and mathematically prove that our programs obey said formulas. The problem is documenting the intent of a rule-based system and confirming that it acts as expected. As every programmer knows, thoroughly defining intended behavior is the meat of impmenting said behavior. Often refining the intent based on thinking through or implementing intermediate solutions. This is not just because of the difficulty to make computers behave the way we want to, it includes the difficulty of defining how we want it to behave, too. There is no silver bullet that can remove ambiguity from human instructions, or always guess "correctly" when missing clear instructions. Because by definition, what is correct?