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.
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.
> . 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.
> 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.
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)
Gatwick long-term parking is not expensive if you book in advance. You need to take a slow bus shuttle to the terminal, but it's never more than 15-20 min including waiting time. I've used it a zillion times as I'd rather not give my keys to those meet & greet companies who drive your car 5 miles. It might void insurance and waiting times when you return tend to be over an hour.
It's sadly becoming harder. I've been playing that game for quite long and hope to stick to web apps, but still.
Some banks limit functionality on web apps, which is annoying.
More importantly, many refuse to provide a decent 2FA other than push notifications inside the app or SMS, which is insecure and EU has mandated its phaseout.
The thing that works for me is to pretend to be clueless and get an old hardware OTP generator, but those are susceptible to impersonation attacks on the bank side.
I think this is the real problem. I am sympathetic towards automated code synthesis.
But without formal verification and a human reviewing specifications to ensure alignment, I think code will end up being broken in unexpected ways or drift away from the original intent.
Discussed in HN many times, but worth restating once more. The N9 was fantastic. A joy to use, and in many ways the best design, both hardware and software, I've ever handled. Everything had been designed with care and some UI elements remain unmatched.
I think I was one of the first developers that got an N770 engineering sample (the first product in the N770-N9 saga) and it was really clear that they were onto something. Sadly, internal politics won over company and consumer interests. It took them extremely long to let this be a phone, not just an "Internet tablet". It was bizarre.
The same team is now behind Jolla/Sailfish. It's pretty remarkable how far they've got, but it's obviously not a perfect product given how small they are compared to the other mobile juggernauts. However, it's usable as a daily driver and, with a critical developer mass, it could get somewhere. There are already quite a few indie apps.
Crucially, I think it's the only platform that has the potential to set you truly free. GrapheneOS is the other alternative I can also endorse and tolerate, but it has a different set of compromises, and it's a bit fragile to Google pulling the plug. But it's great in its own ways.
To add to that: Elop announced the end of N9 weeks before it's release and more then a year before the first Lumina was available. Dead on arrival not even shipped in major markets. Yet the N9 was years ahead any competition of that time.
If you think Chinese companies always act as a bloc, your mental model needs to get about a billion times more detailed. But in this case just a few details may be enough: There are Chinese AI companies that have released LLMs without publishing the weights.
ByteDance is going the direct-to-consumer route with their Doubao chatbot (the most popular in China, probably thanks to their social media prowess). iFlyTek seems to be angling for enterprise and government use cases, where they already have an in.
The companies that have released weights have in common that they didn't have a monetization channel lined up and their models weren't good enough to make people pay attention with just API access. (You can see with Qwen Max that the calculus can change towards not releasing weights for better models.)
And who exactly among the investors is having their complement commoditized? When Nvidia releases Nemotron, the story is clear, but it's less obvious for say Z.ai's GLM.
It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain.
However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language.
Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.
