It has been an area of active research for 40 years. But almost all the research returned the null result, meaning that the program proving didn't improve code quality (basically it didn't work). Yet somehow a group of programmers, usually fresh out of academia falls for program proving each generation. Strong types do really help but you need a good compiler which is sometimes lacking in the real work cough Scala cough. The problem with strong types and program proving is that the juice just isn't worth the squeeze meaning the extra time taken doesn't result in reduced debugging time or improved code quality. I don't think that changes with LLMs. It just exposes the flaws more quickly.
Zuckerberg became rich on php, which grinds my gears almost as much as the genocide thing.
In fairness, my peers at $corp used to ship while I was sad-Wojciech "no you can't create tech debt". The universe is cruel to people who care.
The problem has always been:
- It's extremely labour-intensive, and even small changes to the code can require an enormous amount of new proof work.
- The skills required to formally verify software are very different from the skills required to write it, and the set of people capable of doing so is much smaller.
- Code has to be written with verification in mind, against a specification that expresses invariants that can actually be verified, and that is coherent enough that you can derive useful high-level properties of the system from it.
You needed two teams — verification and development. Verification would always be behind the development team, while also having to feed requirements and design changes back to the developers. Everything slowed to a crawl.
AI changes this. A coherent, verifiable, useful specification isn't easy to write — but it's far easier to write than the software itself, and AI can do most of that work: both drafting the spec and proving that it's consistent and that the high-level properties you actually care about follow from it.
More importantly, a high-level spec is far easier to read and reason about than the reams of code required to actually implement something. Which means:
- AI does the grunt work of writing and proving the spec; humans only have to carefully review that high-level artifact.
- AI writes code it must also prove conforms to the spec, so humans can be assured it's correct without babysitting the AI.
- Changes are driven top-down: evolve the spec first, then have the AI fix the implementation and re-prove conformance.
Our (very, very large) company is rapidly going all-in on formal verification across projects we never would have dreamed of verifying before; the velocity hit and the man-hour cost were only worth paying for truly critical infrastructure.
I suspect you’ve nailed the answer: it’s probably not easy, although it’s also possible that it just hasn’t ever had a lot of attention paid to it because it’s been generally fast enough for their user base?
But in commercial production environments, CI pipelines tend to want to build everything from scratch every time, and that slows everything down. Rust has the same issue. Both languages, by default, compile all their dependencies from source, rather than obtaining precompiled artifacts from a repo the way some languages (like Java) do. And their compilers are slower than e.g. Go's. As the article mentions, various kinds of caching can help with that, but that's extra stuff you have to manage and deal with.
I'm not sure this is a bad thing, though. Haskell co-creator Simon Peyton-Jones coined the unofficial Haskell motto, "avoid success at all costs". I tend to agree with that. It would be difficult for Haskell to maintain its conceptual edge if it were a mainstream commercial language.
You can also limit it with an env var. I have capped mine at 10GB.