I agree with the core thesis that LLMs + theorem provers might make formal methods cheap enough to be practical in software development.

The biggest issue was always cost. But there's still an alignment problem. Without human supervision, things might drift away from the original specification and intent.

From my own experience, what works best is some kind of Hoare/separation logic (contracts), as these are quite easy to follow and decompose.

Even something as simple as a minimal Haskell subset, plus a bit of LiquidHaskell, can get you really far if you are pragmatic.

▲

codebje a day ago | parent | next [-]

IMO the biggest issue was always not knowing what correct is in the first place. The vast majority of software we use, the stuff that's riddled with errors, has those errors largely because what it's supposed to do is vague and never, ever deals with edge cases. You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.

Perhaps that's the same thing as what you're saying, though: we don't specify these things in detail because it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.

▲

saithound 16 hours ago | parent [-]

> . You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions. [..] it's expensive to spend that much time thinking through it all, when users are largely trained to just accept crashes, glitches, inconsistencies, and the occasional sprinkle of data loss.

Indeed. The last bug I fixed in a production app was one where people could not restore from backup due to a de/serialization issue. The correct behavior would have been straightforward to specify (round-tripping). Trying to verify the serializer against the correct behavior would have forced the devs to think through all the edge cases.

	▲	nextos 4 hours ago \| parent [-]
		> You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions. This is why it's so important to separate functional from stateful code. Functional code is generally easier to specify. And, by isolating stateful code, one can e.g. fail fast and avoid stepping into undefined behavior.

▲

nextaccountic 20 hours ago | parent | prev | next [-]

Types, preconditions and theorems are still a guardrail

Agents perform better when programming in Rust than <insert dynamic language here> (at least in my experience), exactly because types matter. Those theorem provers just have a poweful and pedantic type system that insists in being always correct, in detriment of everything else

LiquidHaskell (or flux or creusot in Rust) would be an improvement over Haskell or Rust too.

In either case (full blown theorem provers, or theorem provers laid on top of regular programming languages) the models would need to either focus in posttraining on coming up with good invariants to establish, or you need to prompt agents in a very specific way to get desired results (OP complains that sometimes Claude doesn't want to do this stuff, this happens when it's in out of distribution territory)

▲

pydry 20 hours ago | parent | prev [-]

When I did it the biggest problem is writing the spec. It was longer and more complicated than the code itself.

If you have bugs in the spec you have bugs in the code.