Comment by nanolith
3 years ago
LLMs and other generative AI methods are nowhere near replacing the need for better reasoning about software, especially in safety critical systems.
3 years ago
LLMs and other generative AI methods are nowhere near replacing the need for better reasoning about software, especially in safety critical systems.
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?
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.
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.
4 replies →