7 ms·

We have proof automation now

232 points by zdw 3mo ago

Jhsto 3mo ago
As a meta-comment on the topic, something I have noticed is that there still exists confusion what it means to use theorem provers for projects -- the other day I read a tweet from Paradigm, a crypto-VC now seemingly AI-pilled. Some LP of theirs had made a Lean 4 formalization of the Ethereum's virtual machine. The tweet said this would have cost like $150k in API tokens ("would have", as in, I guess they get theirs for free), and took a week of inference time for an LLM to produce. I somehow got distracted to actually take a look at the code, which I found rather light on theorems. Nor did the project make use of Batteries or Mathlib which are arguably the one of the strongest motivation for me personally to use Lean4. That is, I generally rather rely on someone else getting the category theory and algebraic structures right, which then leaves me the proof obligation to show the correspondence with whatever toy I'm working on. Here I'm fine to use LLMs for proof search, very similar to how would I use a SMT solver. But what I have found is that the language models have to be really coerced into using these libraries, because otherwise the models much rather overfit and overclaim a solution with a 3 minute inference task rather than attempt to fulfill the proof obligations over 3 hours. And I feel nauseated when I need to convince the LLM (I use Claude) that filling the proof obligation is for "academic exercise" or because I'm coerced into doing so, because otherwise it will come up with reasons of its own why it does not want to do it. Now, this happens under the mental model in which I'm interested in finding equivalences with prior work. Many LLM generated Lean code reads more as if someone was interested whether X can be turned into a Lean 4 program, which is mostly yes, and that in general is a positive thing. But, if you are not interested in refinement types and theorems, why not just choose Haskell? The point is, I strongly sense that unless you have good questions to ask, then that's very evident in these languages. And, this is something the LLM won't help you -- if you don't impose a proof obligation for it, it certainly will not try to go the extra mile to conjure one for you.
- Ampersander 3mo ago
  Crypto guys are in the business of grifting magic beans to rubes. They are mostly interested in the aesthetics of these technologies. Using an academic programming language gives these scientific magical vibes and such that make people believe these guys are high tech and know their shit and so on. This is the reason many crypto projects do use Haskell too, it's known as an academic research language that is difficult to use and "if it compiles it works." They come at it from the perspective of "What would sound the best when I try to sell the space money of the future?"
  - pants2 3mo ago
    Blockchain protocols are also faced with the most active, persistent, and well-funded state sponsored attackers of any industry, so naturally formal verification should be of great interest.
nextos 3mo ago
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 3mo ago
  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 3mo ago
    > . 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 2mo ago
rtpg 3mo ago
> We now have LLMs which, combined with proof irrelevance, promise to be an extremely capable form of proof automation. With sufficient amounts of automation perhaps you don't need to worry about proof engineering nearly so much. You still need to avoid blowing up the type checker but, in my limited tests, LLMs can avoid that. Potentially, LLMs suddenly make dependent-type systems dramatically more practical. When I've used interactive proof systems like Roq, I'd often kinda code myself into a hole by cutting along the wrong axes and not specifying my problem in a way that's easy to prove. After all, this is just like in math: you really want to cut at a problem the right way to get to the easy proof. I think people are discounting how important that decision making is. It's not just about whether an LLM can churn through specific proof strategies on a problem, but also about how to pose the problem etc. I'm not saying LLMs can't help, but I think it's less that "proof engineering is not needed" and more that "when these tools are used in the right way, proof engineering is easier". Because at the end of the day these tools work well when they have the right kind of foundations in the first place > AWS made LNSym: a semantics and simulator for AArch64. That's cool. Perhaps we could use it to show equivalence between an optimised assembly implementation of some functions, and their Lean counterparts, and then use the assembly code at run-time? Then we could let LLMs rip at optimisation and they couldn't introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap? Trying to one-shot compcert might be hard! Thinking about it and planning it out might make it easier though...
- vatsachak 3mo ago
  Yeah computer proof writing involves choosing good abstractions at every turn. LLMs aren't great at that yet
  - p-e-w 3mo ago
    That’s true, they’re not great at it. Just better than 99.99% of humans.
    - slopinthebag 3mo ago
      Source?
keithwinstein 3mo ago
This is really cool stuff, and I agree the future is likely to look more like this. I was surprised by the last two paragraphs ("Aside: verified assembly") -- my understanding was that this future is basically already here. I believe agl's colleagues at Google have already deployed some auto-mutated verified assembly versions of some crypto routines, based on the Fiat Crypto + CryptOpt work (https://arxiv.org/pdf/2211.10665 https://arxiv.org/pdf/2211.10665), both involving Andres Erbsen who I think is currently at Google before starting a professorship soon. I dunno if this work would count as "cheap" (it looks like Fig. 10 unfolds over the course of a day) but spending a day auto-exploring many verified-correct machine code implementations of the same routine to find the fastest one (which you then ship forever) doesn't seem impractically expensive either.
kimjune01 3mo ago
as the proof of verification decreases, the value of credentials that act as shortcut proofs of human competence will decrease, too.
ashu1461 3mo ago
This can work for core algorithms for sure, but wondering if this will work for production use cases, production apps come with a lot of edge cases - which are more often than not not logical as well to the point it becomes very hard to document them all in the first place.
- ralusek 3mo ago
  I have had production edge cases anticipated by AI before that I hadn't accounted for.
- munchler 3mo ago
  The flip side is that we currently put programs into production without understanding how they will behave in those edge cases. If you're lucky, they crash and then restart cleanly. If you're unlucky, they silently corrupt data or violate mission-critical invariants.
deadbabe 3mo ago
All this proof automation. But still no P=NP.
- behnamoh 3mo ago
  For P ≠ 0, we get N = 1. ■
gz09 3mo ago
Strongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done. Verus (https://github.com/verus-lang/verus https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).
- Buttons840 3mo ago
  Lean has dependant types. Wouldn't something like Haskell or Idris, that are trying to be general purpose dependantly typed languages--wouldn't they be a better start than versus? Versus appears to just be a formal verification tool. Perhaps I misunderstand? You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used the most (long ago), and the tooling was interactive in a helpful way I've never experienced with other languages. You don't want a separate language used to verify a base language, because then everyone ends up having to know two languages. Looking at the history of computing though, I wouldn't be surprised if this happens. The actual programming language and the verification language can be the same language though, if we want.
  - trenchgun 3mo ago
    Lean4 is a general purpose programming language.
    - singularity2001 3mo ago
      Have you tried writing any programs in it?
      - ndriscoll 2mo ago
        I don't see why it would be particularly difficult beyond not already having a lot of IO libraries (like Kafka connectors or whatever). Pure functional programming in Scala with IO monads is quite pleasant.
davemp 3mo ago
Cool. Now we can write bugs in our theorem descriptions instead of source code. Seriously, please review Curry Howard Isomorphism if you’re getting pulled down this rabbit hole. Programs are proofs. Proofs are programs. So if you can formally describe the correct output for every input, you can have an LLM loop automatically fill in the gaps of how to get there. Congrats, that sounds at least as hard as writing the correct program in most cases. Don’t get me wrong, I do think there are useful tools combining formal methods and llms. Let’s just not get carried away.
- fractorial 3mo ago
  Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!
- 6gvONxR4sf7o 3mo ago
  > Congrats, that sounds at least as hard as writing the correct program in most cases. That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. I can write a formal description of what it means to have property in a way that does have computational content that is equivalent to an algorithm[0], but often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted. The magic is that you can write a spec that's clear, then have the LLM write the code and prove the spec, so you know that given the right inputs/state, it will return the right outputs/state. Then the gap is performance-like characteristics, which is a pretty great starting point and a lot easier to be just empirical about than correctness. [0] in Lean you can also use classical logic or add your own axioms, where it's not even comutational.
  - deleted 3mo ago
    [deleted]
  - davemp 3mo ago
    > That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. Really unnecessary levels of snark here. > often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted Have you ever heard of prolog? I’m sure a prolog program can express whatever property you’re attempting to write just as tersely (if that’s your metric for hard). Almost copy/pastable to and from a theorem proofer. Or are you saying that the program has to be the efficient implementation? Because that’s a different ball game. I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. (At that point we’ll have finally created the fabled “sufficiently smart compiler” and probably solved p=np). A huge majority of software is simple business rules + CRUD that is trivially verifiable. The entire problem is showing that an efficient/reliable program actually implements those rules. > The magic is that you can write a spec that's clear Maybe you can. But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation.
henryrobbins00 3mo ago
I'm very bullish on proof automation as well. I'm currently researching AI for algorithm design and using automated theorem provers to get formal guarantees for generated algorithms. To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback! I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others. [1] https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp [2] https://news.ycombinator.com/item?id=49010310 https://news.ycombinator.com/item?id=49010310 [3] https://news.ycombinator.com/item?id=48780801 https://news.ycombinator.com/item?id=48780801
jason_s 3mo ago
OK so this article is sort of about formal proof automation, but it seems more practically about Zstandard, which I very much enjoyed reading.
- andrewla 3mo ago
  Yeah, this is really cool. I'm now deep in the rabbit hole of FSE encoding and ANS & tANS. The last time I poked my head in here, range encoding and arithmetic encoding were the state of the art for fractional entropy representations, but they both sucked. This is a million times better and so simple that I feel like I should have invented it myself.
m1el 3mo ago
Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) So the cost of finding and developing exploits has dropped dramatically. On the other hand, formal verification is now much easier, since LLMs can automate the proof. You don't even need to worry about hallucinations, you merely need to trust Lean core. If the LLM is wrong, the proof will get rejected! The problem of exploits gets bigger, and the solution of formal verification gets cheaper. As a result, the needle is now moving in the direction of "more formal verification". I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time. My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly. I have not achieved that goal yet. What I have so far: - one (non-optimized) compiler step which is formally verified - three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR https://github.com/m1el/riscv-fv-bootstrap https://github.com/m1el/riscv-fv-bootstrap The project is in quite a bad shape, and I am trying to improve my skills in that direction.
- logicchains 3mo ago
  Have you heard of https://cakeml.org/ https://cakeml.org/? It's a self-hosting formally verified compiler.
  - m1el 3mo ago
    Thank you, I've heard of it. It is indeed very close to what I want to have. CakeML project also has a language Pancake, which has interesting properties. Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/third-party https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...
jabelli31 3mo ago
[flagged]
momentoftop 3mo ago
Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the details by hand. In 1956, Newell came up with the Logic Theorist which was able to prove a decent chunk of the Principia automatically. When Newell informed him, Russell conceded that his manual efforts had turned out to be wasted effort. I used HOL Light about 15 years ago. The vast majority of the proof details are done by a machine, generally split between term rewriting and then offloads to a generic automated prover for first-order logic. Your job then is formalising the theorem statements and orchestrating the automation, and the latter still takes an enormous amount of labour. Around this time, we were getting excited about recommender systems for lemma selection. The idea was that you turn every theorem into a bunch of features and train a recommender system against the lemma needed to prove it. Then when you face a new problem, you use its features to recommend which lemmas are likely to be needed. You then throw those lemmas and your conjecture at a bunch of industrial strength automated provers, get the provers to come back with a minimal set of necessary lemmas, and then use your verified automated prover to do the real proof with a tractable set of inputs. It first got implemented in Isabelle/HOL as Sledgehammer, and was a massive improvement to tooling. Now LLMs are here and the game looks completely different. I went back over some verification I spent a week on about 5 years ago, in a pretty obscure formal verifier called HOL Light, on a problem of my own making. I'd seen how terrible ChatGPT was at propositional logic a few years back, so this is the sort of thing I'd had in my back-pocket as an "impossible benchmark" for LLMs. So as a half-joke, I gave Claude the main theorem I wanted proving, hoping to watch it embarrass itself. In a minute or two, it has come up with the same proof strategy I had used, proving four lemmas to get to the main theorem. This was impressive, but that's not the laborious part, and I was pretty confident it would die trying to prove just the first lemma. It has its four lemmas enumerated and goes to thinking, while I go off for a cup of tea. I come back five minutes later and it has scratched off the first goal. I'm pretty shaken, and go off again trying to process that. Come back, the second goal has gone. And then the third. And then the fourth. And then, after just fifteen minutes, it's pulled off a week of my work, done it more efficiently, and near enough one-shotted each proof. That took me a while to process. I realised that if I had this 15 years ago, it would have done 95% of my PhD, which is to say that 15 years ago, I would have done a 20x more ambitious thesis. I contacted my old supervisor, who said the theorem proving community are all on top of this, including the creator of HOL Light, now at AWS. HOL Light, incidentally, was used on what I still believe is the most ambitious mathematical theorem proving project to date, the verification of the Kepler Conjecture. The lead on that project recruited a team to get the proof through over about 5 years. Today, I wouldn't be surprised if he could have solo'd it in 6 months. The same goes for another extremely ambitious project, the verification of the seL4 microkernel. And for another open problem, I know there are people seriously wanting to get a verification of Fermat's Last Theorem, which sounded delusional 15 years ago, but sounds pretty plausible now. Exactly where this goes, I am not sure. I suspect we can now start on verification projects that would have been insane to contemplate. But a few things concern me. One is that Lean seems to have all the mind-share. Maybe it deserves it, but there are very major and mature theorem proving technologies such as Coq (now Rocq), Isabelle, HOL Light, ACL2 and Mizar that I believe still win in terms of having the largest verification libraries and the biggest verified projects. These should not be forgotten about, since they will also probably have the most training data, having been going for many decades now. The second is that verifying our crappy human specifications probably isn't going to fly. As the creator of HOL Light says, representation (how you formalise your problem domain) is still where it all matters, and the LLMs aren't very good at this. And neither are the writers of our current specs. Verifying that a piece of software meets the HTTP spec will be considered an achievement, but it's the wrong goal. We'll need specifications that are modular and composable, that mesh together so that each piece is sanity checking the others. This is how we build mathematics, and it's how we'd need to build software. Specs need to be short and comprehensible, so that a human can verify them. If your spec is as long and complex as the implementation, it's worthless. But I believe it is possible to design software from the ground up where the motivation is specification engineering rather than code engineering, and thereby the specifications become the only human-facing understandable part of software. The implementation is just some artifact that an LLM generates that nobody looks at unless they are curious. And I think LLMS today mean that "build the world over again" isn't as mad a thought as it used to be.
madhu_ghalame 3mo ago
[dead]
anilgulecha 3mo ago
I'm convinced Math is the canary for what's going to happen to knowledge work. Coding was ahead in harnessing early LLM capability, but Math, given it's pure form, has aleady racing ahead. The dimensions to notice are: Research speedup, practitioner expertize, labour dynamics, junior entrants, world impact. In that sense it's a canary, whatever happens to Math, will in order flow to other sciences in-order of purity: Computer science, physics, chem, bio, social sciences.
- logicchains 3mo ago
  Math is the opposite of a canary because it's possible to generate infinite amounts of synthetic training data for it, unlike almost every other kind of knowledge work where correctness depends on external input.
  - anilgulecha 3mo ago
    That's why it's a canary - because it has minimal external input, and most pure. External inputs are bound get LLM friendlier with time, in the order I mentioned above.
  - deleted 2mo ago
    [deleted]
el_pollo_diablo 3mo ago
I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, with more elaborate properties and longer proofs. Suddenly, you realize that you need to prove a new property of your program. Can you keep your existing work and build on top of it? In general, no, you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program. That is because dependent types (and other staples of naive approaches to proving program properties, like a unique invariant per loop) structure the program along the wrong dimension: they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it") or a program point ("write the precondition for this function as a big conjunction mixing all the concerns"), where it works much better, for long-term maintenance, to structure the development along concerns: computational parts of the program, basic functional properties and absence of UB, termination, other functional properties, security, etc., where each layer builds on top of the previous ones without requiring them to change. That is not to say that dependent types do not have their use. Where they shine is at module boundaries. Consider a library that exposes an opaque type and operations on it. Users of the library can only build and modify values of that type through the library's API. This type should be a dependent type. If it needs to be refined at any point to encode a new invariant, this will have no impact on the library's users, since all they do is pass around values without interpreting them. However, inside the library, I would recommend unpacking/repacking the dependent type at the library's entry points and handling the concerns separately.
- prplfsh 3mo ago
  It's my own ignorance speaking, but is this as true in math? I could see this being a problem for programs where you have few, if any, real axioms and the axioms themselves change. But if we're talking math, the axioms should be fixed.
  - 3mo ago
hnlb53nrpg 3mo ago
Exactly the reminder I needed
colechristensen 3mo ago
I think people are overestimating the usefulness LLMs will bring us based on early examples of low hanging fruit being harvested. LLMs have a VERY different set of things which are easy and which are hard and from software security to math proofs we're seeing very early impressive results but those will run out and new classes of what is difficult will show themselves. The "this new tech will cause everything to be easy from now on!" feeling has happened many times before and always new limitations were found. Industrialization was thought to be basically the end of the need for money or significant labor during the industrial revolution (this optimism is where communism came from) and that future never came. The same will be here: rapid change but also new limitations which are still hard to imagine.
- rafaelRiv 3mo ago
  I program very often in idris2 and I cannot agree more. LLMs tend to take the least effort possible to the point where most of the time, llms are just not useful to program with dependent types. At least, not yet
  - vatsachak 3mo ago
    Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions
    - rafaelRiv 3mo ago
      I do but I have no guarantee that the llms will make a sane implementation of the types
      - dleink 2mo ago
        You still want to write/review/refine the types yourself.
andai 3mo ago
I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details. Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was pointless and completely defeated the purpose. (An LLM also pointed that out, so I guess it must have been a different one which implemented it? I'm trying to get them to sign their names in the commits...) These new models are very thorough and responsible however, so of course it had written a copious number of tests, and of course all the tests passed! I found this very amusing. It had diligently proven the correctness of the incorrect functionality!* I've been thinking about how cool it is the AI can assist with writing proofs now, and how we can use this new ability to boost the correctness of our code. It later occurred to me, however, that formal verification would not have helped in this case. It would have just formally verified that the wrong thing was correct! -- *Yeah I know tests prove the presence of bugs but not their absence. Couldn't think of a better way to phrase that though.
- david-gpu 3mo ago
  I had a college professor do the exact same thing in class: he made a fairly subtle mistake formalizing his specification, and thus his proof was perfect but did not solve the actual problem he was trying to address. He was a mathematician and was convinced that formal methods were the future of software engineering. He also loved handwaving that due to Godel's incompleteness theorem, humans were necessary to introduce creative insights (new axioms) that computers would never be able to do. I eventually obtained top marks both semesters and left convinced that formal methods are a waste of time in >99% of the cases.
- justincormack 3mo ago
  re "An LLM also pointed that out, so I guess it must have been a different one which implemented it?" - no, there is no correlation between whether the same LLM is used and whether it can find errors.
- chrisjj 3mo ago
eru 3mo ago
The article says that their zstd decoder is 10x slower than the 'normal' one. I would be interested in seeing if that can be driven down to (almost) parity, with a bit more LLM time and perhaps human effort.
pjmlp 3mo ago
> Aside: verified assembly This isn't new, it is actually part of how Dafny came to be, another formal verification programming language. "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System" https://www.microsoft.com/en-us/research/publication/safe-to-the-last-instruction-automated-verification-of-a-type-safe-operating-system https://www.microsoft.com/en-us/research/publication/safe-to... However so far hardly anyone in mainstram cared about verified assembly, maybe now with LLMs. "Programming Language Design and Implementation in the Era of Machine Learning" https://www.youtube.com/watch?v=Fc3cW0nqAQ0 https://www.youtube.com/watch?v=Fc3cW0nqAQ0
vessenes 3mo ago
I think it's worth putting a Knuth quote up on your board when you think about verification as an end goal: "Beware of bugs in the above code; I have only proved it correct, not tried it." Or, as Wolfram proposes in another link on the front page today, the irreducibility of computation means we cannot generally get all bugs out of systems. To my mind, one of the risks of going all in on verification is that you just move the difficulty to a harder, more abstract layer - the specification. In my experience, this typically looks appealing to a 'type' -- very high IQ, very little real world engineering experience -- it's a dream that hits the inevitable grittiness of the real world and .. the real world keeps winning.
- whoke 2mo ago
  I like the concept of "inevitable grittiness"! I think languages like Lean actually do a very nice job of pushing the grittiness out to the boundaries of your program. Everything else can stay pure, and in domains that are amenable to mathematical reasoning (compilers, DSP, etc) it feels like a natural fit. I don't think you have to go all in, either. I ported the compiler project I'm working on from TypeScript to Lean and recently spent a weekend making all the functions total and implementing a few basic theorems. On a basic level it feels like writing Haskell, but there's a lot more room to grow with it.
1970-01-01 3mo ago
Makes me wonder if we should just be dumping some tokens into decades and decades of stale code to formally verify and then Fix-It-Forever (TM) because the alternative is waiting around for it to be broken.
dmix 3mo ago
> I've long had a soft spot for dependently-typed languages Whatever happened to Idris? Is that still being developed? Edit: Looks like they are working on Idris 2 https://github.com/idris-lang/Idris2 https://github.com/idris-lang/Idris2
monarchwadia 2mo ago
Proof automation will make things a lot easier. I'm not entirely sure that it's the only thing required, but it's a big part of the thing required. What's more interesting to me is, how do we prove that the business intent is accurately encoded in the code? This is a different problem. Not "is the logic internally coherent," but "is the logic going to give us what we want?" And how do we make sure that the logic keeps giving us what we want, iteration after iteration? I've open source a tool, Drift, for this purpose. So far, biased and anecdotally as its builder, this has been the missing layer. It works because the spec is treated as a duplicate of the code, written and committed in the repo and kept in sync with hashes. The LLM then checks for diffs manually. There are ways to use perplexity here as well. Here is an article about how to get started. https://monarchwadia.medium.com/how-to-make-your-agent-more-reliable-with-spec-files-493a4281091f https://monarchwadia.medium.com/how-to-make-your-agent-more-... Doubtless, many more automations will come. We live in very exciting times. It has been a while since a new technology affected every corner of software engineering with such depth of change. This might be unprecedented.
nlogn_alltheway 2mo ago
I just feel an existential angst, are we damned to keep reinventing the same wheel? Static contracts and proofs are basically solved for industrial use in SPARK, yet somehow we keep reinventing. Is computer science really engineering? We don’t stand on the shoulders of giants, every new generation has the urge to invent a leave a mark. This in itself is great, except that, in contrast to other branches of engineering (say mechanical, or structural) previous know how is ignored and disregarded. Perhaps there is too much of it, and SNR these days is too low, impossible to be held in one’s head. Perhaps it’s easier these days with LLMs to survey what’s done. Yet the slop waves keep crashing on us. We have seen this with dbs. The relational model layed the foundations. Yet periodically a new craze emerges. Everyone’s chases the latest cool new thing, until the ugly warts that were know to be there decades ago resurface and become real blockers (looking at you mongo). Yet another post about program proofs, yet no mention of the only industrial strength, actually practical and pleasant to use formal verification language: SPARK.

232 points by zdw 3mo ago

Jhsto 3mo ago

As a meta-comment on the topic, something I have noticed is that there still exists confusion what it means to use theorem provers for projects -- the other day I read a tweet from Paradigm, a crypto-VC now seemingly AI-pilled. Some LP of theirs had made a Lean 4 formalization of the Ethereum's virtual machine. The tweet said this would have cost like $150k in API tokens ("would have", as in, I guess they get theirs for free), and took a week of inference time for an LLM to produce. I somehow got distracted to actually take a look at the code, which I found rather light on theorems. Nor did the project make use of Batteries or Mathlib which are arguably the one of the strongest motivation for me personally to use Lean4. That is, I generally rather rely on someone else getting the category theory and algebraic structures right, which then leaves me the proof obligation to show the correspondence with whatever toy I'm working on. Here I'm fine to use LLMs for proof search, very similar to how would I use a SMT solver. But what I have found is that the language models have to be really coerced into using these libraries, because otherwise the models much rather overfit and overclaim a solution with a 3 minute inference task rather than attempt to fulfill the proof obligations over 3 hours. And I feel nauseated when I need to convince the LLM (I use Claude) that filling the proof obligation is for "academic exercise" or because I'm coerced into doing so, because otherwise it will come up with reasons of its own why it does not want to do it. Now, this happens under the mental model in which I'm interested in finding equivalences with prior work. Many LLM generated Lean code reads more as if someone was interested whether X can be turned into a Lean 4 program, which is mostly yes, and that in general is a positive thing. But, if you are not interested in refinement types and theorems, why not just choose Haskell? The point is, I strongly sense that unless you have good questions to ask, then that's very evident in these languages. And, this is something the LLM won't help you -- if you don't impose a proof obligation for it, it certainly will not try to go the extra mile to conjure one for you.

Ampersander 3mo ago
Crypto guys are in the business of grifting magic beans to rubes. They are mostly interested in the aesthetics of these technologies. Using an academic programming language gives these scientific magical vibes and such that make people believe these guys are high tech and know their shit and so on. This is the reason many crypto projects do use Haskell too, it's known as an academic research language that is difficult to use and "if it compiles it works." They come at it from the perspective of "What would sound the best when I try to sell the space money of the future?"
- pants2 3mo ago
  Blockchain protocols are also faced with the most active, persistent, and well-funded state sponsored attackers of any industry, so naturally formal verification should be of great interest.

nextos 3mo ago

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 3mo ago
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 3mo ago
  > . 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 2mo ago

rtpg 3mo ago

> We now have LLMs which, combined with proof irrelevance, promise to be an extremely capable form of proof automation. With sufficient amounts of automation perhaps you don't need to worry about proof engineering nearly so much. You still need to avoid blowing up the type checker but, in my limited tests, LLMs can avoid that. Potentially, LLMs suddenly make dependent-type systems dramatically more practical. When I've used interactive proof systems like Roq, I'd often kinda code myself into a hole by cutting along the wrong axes and not specifying my problem in a way that's easy to prove. After all, this is just like in math: you really want to cut at a problem the right way to get to the easy proof. I think people are discounting how important that decision making is. It's not just about whether an LLM can churn through specific proof strategies on a problem, but also about how to pose the problem etc. I'm not saying LLMs can't help, but I think it's less that "proof engineering is not needed" and more that "when these tools are used in the right way, proof engineering is easier". Because at the end of the day these tools work well when they have the right kind of foundations in the first place > AWS made LNSym: a semantics and simulator for AArch64. That's cool. Perhaps we could use it to show equivalence between an optimised assembly implementation of some functions, and their Lean counterparts, and then use the assembly code at run-time? Then we could let LLMs rip at optimisation and they couldn't introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap? Trying to one-shot compcert might be hard! Thinking about it and planning it out might make it easier though...

vatsachak 3mo ago
Yeah computer proof writing involves choosing good abstractions at every turn. LLMs aren't great at that yet
- p-e-w 3mo ago
  That’s true, they’re not great at it. Just better than 99.99% of humans.
  - slopinthebag 3mo ago
    Source?

keithwinstein 3mo ago

This is really cool stuff, and I agree the future is likely to look more like this. I was surprised by the last two paragraphs ("Aside: verified assembly") -- my understanding was that this future is basically already here. I believe agl's colleagues at Google have already deployed some auto-mutated verified assembly versions of some crypto routines, based on the Fiat Crypto + CryptOpt work (https://arxiv.org/pdf/2211.10665 https://arxiv.org/pdf/2211.10665), both involving Andres Erbsen who I think is currently at Google before starting a professorship soon. I dunno if this work would count as "cheap" (it looks like Fig. 10 unfolds over the course of a day) but spending a day auto-exploring many verified-correct machine code implementations of the same routine to find the fastest one (which you then ship forever) doesn't seem impractically expensive either.

kimjune01 3mo ago

as the proof of verification decreases, the value of credentials that act as shortcut proofs of human competence will decrease, too.

ashu1461 3mo ago

This can work for core algorithms for sure, but wondering if this will work for production use cases, production apps come with a lot of edge cases - which are more often than not not logical as well to the point it becomes very hard to document them all in the first place.

ralusek 3mo ago
I have had production edge cases anticipated by AI before that I hadn't accounted for.
munchler 3mo ago
The flip side is that we currently put programs into production without understanding how they will behave in those edge cases. If you're lucky, they crash and then restart cleanly. If you're unlucky, they silently corrupt data or violate mission-critical invariants.

deadbabe 3mo ago

All this proof automation. But still no P=NP.

behnamoh 3mo ago
For P ≠ 0, we get N = 1. ■

gz09 3mo ago

Strongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done. Verus (https://github.com/verus-lang/verus https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).

Buttons840 3mo ago
Lean has dependant types. Wouldn't something like Haskell or Idris, that are trying to be general purpose dependantly typed languages--wouldn't they be a better start than versus? Versus appears to just be a formal verification tool. Perhaps I misunderstand? You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used the most (long ago), and the tooling was interactive in a helpful way I've never experienced with other languages. You don't want a separate language used to verify a base language, because then everyone ends up having to know two languages. Looking at the history of computing though, I wouldn't be surprised if this happens. The actual programming language and the verification language can be the same language though, if we want.
- trenchgun 3mo ago
  Lean4 is a general purpose programming language.
  - singularity2001 3mo ago
    Have you tried writing any programs in it?
    - ndriscoll 2mo ago
      I don't see why it would be particularly difficult beyond not already having a lot of IO libraries (like Kafka connectors or whatever). Pure functional programming in Scala with IO monads is quite pleasant.

davemp 3mo ago

Cool. Now we can write bugs in our theorem descriptions instead of source code. Seriously, please review Curry Howard Isomorphism if you’re getting pulled down this rabbit hole. Programs are proofs. Proofs are programs. So if you can formally describe the correct output for every input, you can have an LLM loop automatically fill in the gaps of how to get there. Congrats, that sounds at least as hard as writing the correct program in most cases. Don’t get me wrong, I do think there are useful tools combining formal methods and llms. Let’s just not get carried away.

fractorial 3mo ago
Pretty much this. I designed my own research harness and infra for theorem proving and conjecturing; however, you still need to review formulations!
6gvONxR4sf7o 3mo ago
> Congrats, that sounds at least as hard as writing the correct program in most cases. That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. I can write a formal description of what it means to have property in a way that does have computational content that is equivalent to an algorithm[0], but often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted. The magic is that you can write a spec that's clear, then have the LLM write the code and prove the spec, so you know that given the right inputs/state, it will return the right outputs/state. Then the gap is performance-like characteristics, which is a pretty great starting point and a lot easier to be just empirical about than correctness. [0] in Lean you can also use classical logic or add your own axioms, where it's not even comutational.
- deleted 3mo ago
  [deleted]
- davemp 3mo ago
  > That's not remotely true. Or, more formally speaking since we're in a thread about proof assistants, it's not remotely true, up to extensional equality, plus some choices about which axioms you use. Really unnecessary levels of snark here. > often the clearest way to express the property is equivalent to an algorithm that literally brute forces the problem, like sorting a thing by checking every permutation until you find one that's sorted Have you ever heard of prolog? I’m sure a prolog program can express whatever property you’re attempting to write just as tersely (if that’s your metric for hard). Almost copy/pastable to and from a theorem proofer. Or are you saying that the program has to be the efficient implementation? Because that’s a different ball game. I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms. (At that point we’ll have finally created the fabled “sufficiently smart compiler” and probably solved p=np). A huge majority of software is simple business rules + CRUD that is trivially verifiable. The entire problem is showing that an efficient/reliable program actually implements those rules. > The magic is that you can write a spec that's clear Maybe you can. But I did spend a grad class with rocq (coq at the time) and a decade working with “systems engineers” and am not convinced that this is a realistic expectation.

henryrobbins00 3mo ago

I'm very bullish on proof automation as well. I'm currently researching AI for algorithm design and using automated theorem provers to get formal guarantees for generated algorithms. To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback! I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others. [1] https://github.com/henryrobbins/open-atp https://github.com/henryrobbins/open-atp [2] https://news.ycombinator.com/item?id=49010310 https://news.ycombinator.com/item?id=49010310 [3] https://news.ycombinator.com/item?id=48780801 https://news.ycombinator.com/item?id=48780801

jason_s 3mo ago

OK so this article is sort of about formal proof automation, but it seems more practically about Zstandard, which I very much enjoyed reading.

andrewla 3mo ago
Yeah, this is really cool. I'm now deep in the rabbit hole of FSE encoding and ANS & tANS. The last time I poked my head in here, range encoding and arithmetic encoding were the state of the art for fractional entropy representations, but they both sucked. This is a million times better and so simple that I feel like I should have invented it myself.

m1el 3mo ago

Self-insert time. I spent some time exploring this topic. Here's my thesis: Formal verification was expensive. 20x expensive compared to just developing the software, as the author notes. The cost of finding and developing exploits also was high. That creates an incentive to put software verification aside, since it solves a relatively small problem, at an extremely high cost. We've seen how Mythos has found more vulnerabilities than the rest of the security industry combined. (you can argue about the quality and what counts as a vulnerability, but not the point) So the cost of finding and developing exploits has dropped dramatically. On the other hand, formal verification is now much easier, since LLMs can automate the proof. You don't even need to worry about hallucinations, you merely need to trust Lean core. If the LLM is wrong, the proof will get rejected! The problem of exploits gets bigger, and the solution of formal verification gets cheaper. As a result, the needle is now moving in the direction of "more formal verification". I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time. My (ambitious) goal is to have a self-hosting, formally verified compiler, which allows proof transfer from source code down to assembly. I have not achieved that goal yet. What I have so far: - one (non-optimized) compiler step which is formally verified - three simple functions (hex, hex with labels, strtoull) formally verified, against RISC-V assembly, and against a custom IR https://github.com/m1el/riscv-fv-bootstrap https://github.com/m1el/riscv-fv-bootstrap The project is in quite a bad shape, and I am trying to improve my skills in that direction.

logicchains 3mo ago
Have you heard of https://cakeml.org/ https://cakeml.org/? It's a self-hosting formally verified compiler.
- m1el 3mo ago
  Thank you, I've heard of it. It is indeed very close to what I want to have. CakeML project also has a language Pancake, which has interesting properties. Here's the list of projects which I'm aware of: https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/third-party https://github.com/m1el/riscv-fv-bootstrap/tree/master/docs/...

jabelli31 3mo ago

[flagged]

momentoftop 3mo ago

Theorem provers have always made extensive use of AI and automation. Formal logic is insanely laborious, and it took Russell a monumental effort to not get very far with his manual verifications in Principia Mathematica, working out all the details by hand. In 1956, Newell came up with the Logic Theorist which was able to prove a decent chunk of the Principia automatically. When Newell informed him, Russell conceded that his manual efforts had turned out to be wasted effort. I used HOL Light about 15 years ago. The vast majority of the proof details are done by a machine, generally split between term rewriting and then offloads to a generic automated prover for first-order logic. Your job then is formalising the theorem statements and orchestrating the automation, and the latter still takes an enormous amount of labour. Around this time, we were getting excited about recommender systems for lemma selection. The idea was that you turn every theorem into a bunch of features and train a recommender system against the lemma needed to prove it. Then when you face a new problem, you use its features to recommend which lemmas are likely to be needed. You then throw those lemmas and your conjecture at a bunch of industrial strength automated provers, get the provers to come back with a minimal set of necessary lemmas, and then use your verified automated prover to do the real proof with a tractable set of inputs. It first got implemented in Isabelle/HOL as Sledgehammer, and was a massive improvement to tooling. Now LLMs are here and the game looks completely different. I went back over some verification I spent a week on about 5 years ago, in a pretty obscure formal verifier called HOL Light, on a problem of my own making. I'd seen how terrible ChatGPT was at propositional logic a few years back, so this is the sort of thing I'd had in my back-pocket as an "impossible benchmark" for LLMs. So as a half-joke, I gave Claude the main theorem I wanted proving, hoping to watch it embarrass itself. In a minute or two, it has come up with the same proof strategy I had used, proving four lemmas to get to the main theorem. This was impressive, but that's not the laborious part, and I was pretty confident it would die trying to prove just the first lemma. It has its four lemmas enumerated and goes to thinking, while I go off for a cup of tea. I come back five minutes later and it has scratched off the first goal. I'm pretty shaken, and go off again trying to process that. Come back, the second goal has gone. And then the third. And then the fourth. And then, after just fifteen minutes, it's pulled off a week of my work, done it more efficiently, and near enough one-shotted each proof. That took me a while to process. I realised that if I had this 15 years ago, it would have done 95% of my PhD, which is to say that 15 years ago, I would have done a 20x more ambitious thesis. I contacted my old supervisor, who said the theorem proving community are all on top of this, including the creator of HOL Light, now at AWS. HOL Light, incidentally, was used on what I still believe is the most ambitious mathematical theorem proving project to date, the verification of the Kepler Conjecture. The lead on that project recruited a team to get the proof through over about 5 years. Today, I wouldn't be surprised if he could have solo'd it in 6 months. The same goes for another extremely ambitious project, the verification of the seL4 microkernel. And for another open problem, I know there are people seriously wanting to get a verification of Fermat's Last Theorem, which sounded delusional 15 years ago, but sounds pretty plausible now. Exactly where this goes, I am not sure. I suspect we can now start on verification projects that would have been insane to contemplate. But a few things concern me. One is that Lean seems to have all the mind-share. Maybe it deserves it, but there are very major and mature theorem proving technologies such as Coq (now Rocq), Isabelle, HOL Light, ACL2 and Mizar that I believe still win in terms of having the largest verification libraries and the biggest verified projects. These should not be forgotten about, since they will also probably have the most training data, having been going for many decades now. The second is that verifying our crappy human specifications probably isn't going to fly. As the creator of HOL Light says, representation (how you formalise your problem domain) is still where it all matters, and the LLMs aren't very good at this. And neither are the writers of our current specs. Verifying that a piece of software meets the HTTP spec will be considered an achievement, but it's the wrong goal. We'll need specifications that are modular and composable, that mesh together so that each piece is sanity checking the others. This is how we build mathematics, and it's how we'd need to build software. Specs need to be short and comprehensible, so that a human can verify them. If your spec is as long and complex as the implementation, it's worthless. But I believe it is possible to design software from the ground up where the motivation is specification engineering rather than code engineering, and thereby the specifications become the only human-facing understandable part of software. The implementation is just some artifact that an LLM generates that nobody looks at unless they are curious. And I think LLMS today mean that "build the world over again" isn't as mad a thought as it used to be.

madhu_ghalame 3mo ago

[dead]

anilgulecha 3mo ago

I'm convinced Math is the canary for what's going to happen to knowledge work. Coding was ahead in harnessing early LLM capability, but Math, given it's pure form, has aleady racing ahead. The dimensions to notice are: Research speedup, practitioner expertize, labour dynamics, junior entrants, world impact. In that sense it's a canary, whatever happens to Math, will in order flow to other sciences in-order of purity: Computer science, physics, chem, bio, social sciences.

logicchains 3mo ago
Math is the opposite of a canary because it's possible to generate infinite amounts of synthetic training data for it, unlike almost every other kind of knowledge work where correctness depends on external input.
- anilgulecha 3mo ago
  That's why it's a canary - because it has minimal external input, and most pure. External inputs are bound get LLM friendlier with time, in the order I mentioned above.
- deleted 2mo ago
  [deleted]

el_pollo_diablo 3mo ago

I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible. Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, with more elaborate properties and longer proofs. Suddenly, you realize that you need to prove a new property of your program. Can you keep your existing work and build on top of it? In general, no, you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program. That is because dependent types (and other staples of naive approaches to proving program properties, like a unique invariant per loop) structure the program along the wrong dimension: they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it") or a program point ("write the precondition for this function as a big conjunction mixing all the concerns"), where it works much better, for long-term maintenance, to structure the development along concerns: computational parts of the program, basic functional properties and absence of UB, termination, other functional properties, security, etc., where each layer builds on top of the previous ones without requiring them to change. That is not to say that dependent types do not have their use. Where they shine is at module boundaries. Consider a library that exposes an opaque type and operations on it. Users of the library can only build and modify values of that type through the library's API. This type should be a dependent type. If it needs to be refined at any point to encode a new invariant, this will have no impact on the library's users, since all they do is pass around values without interpreting them. However, inside the library, I would recommend unpacking/repacking the dependent type at the library's entry points and handling the concerns separately.

prplfsh 3mo ago
It's my own ignorance speaking, but is this as true in math? I could see this being a problem for programs where you have few, if any, real axioms and the axioms themselves change. But if we're talking math, the axioms should be fixed.
- 3mo ago

hnlb53nrpg 3mo ago

Exactly the reminder I needed

colechristensen 3mo ago

I think people are overestimating the usefulness LLMs will bring us based on early examples of low hanging fruit being harvested. LLMs have a VERY different set of things which are easy and which are hard and from software security to math proofs we're seeing very early impressive results but those will run out and new classes of what is difficult will show themselves. The "this new tech will cause everything to be easy from now on!" feeling has happened many times before and always new limitations were found. Industrialization was thought to be basically the end of the need for money or significant labor during the industrial revolution (this optimism is where communism came from) and that future never came. The same will be here: rapid change but also new limitations which are still hard to imagine.

rafaelRiv 3mo ago
I program very often in idris2 and I cannot agree more. LLMs tend to take the least effort possible to the point where most of the time, llms are just not useful to program with dependent types. At least, not yet
- vatsachak 3mo ago
  Have you tried giving them the types you want and then have them auto complete? They are pretty good at a auto completing abstractions
  - rafaelRiv 3mo ago
    I do but I have no guarantee that the llms will make a sane implementation of the types
    - dleink 2mo ago
      You still want to write/review/refine the types yourself.

andai 3mo ago

I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details. Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was pointless and completely defeated the purpose. (An LLM also pointed that out, so I guess it must have been a different one which implemented it? I'm trying to get them to sign their names in the commits...) These new models are very thorough and responsible however, so of course it had written a copious number of tests, and of course all the tests passed! I found this very amusing. It had diligently proven the correctness of the incorrect functionality!* I've been thinking about how cool it is the AI can assist with writing proofs now, and how we can use this new ability to boost the correctness of our code. It later occurred to me, however, that formal verification would not have helped in this case. It would have just formally verified that the wrong thing was correct! -- *Yeah I know tests prove the presence of bugs but not their absence. Couldn't think of a better way to phrase that though.

david-gpu 3mo ago
I had a college professor do the exact same thing in class: he made a fairly subtle mistake formalizing his specification, and thus his proof was perfect but did not solve the actual problem he was trying to address. He was a mathematician and was convinced that formal methods were the future of software engineering. He also loved handwaving that due to Godel's incompleteness theorem, humans were necessary to introduce creative insights (new axioms) that computers would never be able to do. I eventually obtained top marks both semesters and left convinced that formal methods are a waste of time in >99% of the cases.
justincormack 3mo ago
re "An LLM also pointed that out, so I guess it must have been a different one which implemented it?" - no, there is no correlation between whether the same LLM is used and whether it can find errors.
chrisjj 3mo ago

eru 3mo ago

The article says that their zstd decoder is 10x slower than the 'normal' one. I would be interested in seeing if that can be driven down to (almost) parity, with a bit more LLM time and perhaps human effort.

pjmlp 3mo ago

> Aside: verified assembly This isn't new, it is actually part of how Dafny came to be, another formal verification programming language. "Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System" https://www.microsoft.com/en-us/research/publication/safe-to-the-last-instruction-automated-verification-of-a-type-safe-operating-system https://www.microsoft.com/en-us/research/publication/safe-to... However so far hardly anyone in mainstram cared about verified assembly, maybe now with LLMs. "Programming Language Design and Implementation in the Era of Machine Learning" https://www.youtube.com/watch?v=Fc3cW0nqAQ0 https://www.youtube.com/watch?v=Fc3cW0nqAQ0

vessenes 3mo ago

I think it's worth putting a Knuth quote up on your board when you think about verification as an end goal: "Beware of bugs in the above code; I have only proved it correct, not tried it." Or, as Wolfram proposes in another link on the front page today, the irreducibility of computation means we cannot generally get all bugs out of systems. To my mind, one of the risks of going all in on verification is that you just move the difficulty to a harder, more abstract layer - the specification. In my experience, this typically looks appealing to a 'type' -- very high IQ, very little real world engineering experience -- it's a dream that hits the inevitable grittiness of the real world and .. the real world keeps winning.

whoke 2mo ago
I like the concept of "inevitable grittiness"! I think languages like Lean actually do a very nice job of pushing the grittiness out to the boundaries of your program. Everything else can stay pure, and in domains that are amenable to mathematical reasoning (compilers, DSP, etc) it feels like a natural fit. I don't think you have to go all in, either. I ported the compiler project I'm working on from TypeScript to Lean and recently spent a weekend making all the functions total and implementing a few basic theorems. On a basic level it feels like writing Haskell, but there's a lot more room to grow with it.

1970-01-01 3mo ago

Makes me wonder if we should just be dumping some tokens into decades and decades of stale code to formally verify and then Fix-It-Forever (TM) because the alternative is waiting around for it to be broken.

dmix 3mo ago

> I've long had a soft spot for dependently-typed languages Whatever happened to Idris? Is that still being developed? Edit: Looks like they are working on Idris 2 https://github.com/idris-lang/Idris2 https://github.com/idris-lang/Idris2

monarchwadia 2mo ago

Proof automation will make things a lot easier. I'm not entirely sure that it's the only thing required, but it's a big part of the thing required. What's more interesting to me is, how do we prove that the business intent is accurately encoded in the code? This is a different problem. Not "is the logic internally coherent," but "is the logic going to give us what we want?" And how do we make sure that the logic keeps giving us what we want, iteration after iteration? I've open source a tool, Drift, for this purpose. So far, biased and anecdotally as its builder, this has been the missing layer. It works because the spec is treated as a duplicate of the code, written and committed in the repo and kept in sync with hashes. The LLM then checks for diffs manually. There are ways to use perplexity here as well. Here is an article about how to get started. https://monarchwadia.medium.com/how-to-make-your-agent-more-reliable-with-spec-files-493a4281091f https://monarchwadia.medium.com/how-to-make-your-agent-more-... Doubtless, many more automations will come. We live in very exciting times. It has been a while since a new technology affected every corner of software engineering with such depth of change. This might be unprecedented.

nlogn_alltheway 2mo ago

I just feel an existential angst, are we damned to keep reinventing the same wheel? Static contracts and proofs are basically solved for industrial use in SPARK, yet somehow we keep reinventing. Is computer science really engineering? We don’t stand on the shoulders of giants, every new generation has the urge to invent a leave a mark. This in itself is great, except that, in contrast to other branches of engineering (say mechanical, or structural) previous know how is ignored and disregarded. Perhaps there is too much of it, and SNR these days is too low, impossible to be held in one’s head. Perhaps it’s easier these days with LLMs to survey what’s done. Yet the slop waves keep crashing on us. We have seen this with dbs. The relational model layed the foundations. Yet periodically a new craze emerges. Everyone’s chases the latest cool new thing, until the ugly warts that were know to be there decades ago resurface and become real blockers (looking at you mongo). Yet another post about program proofs, yet no mention of the only industrial strength, actually practical and pleasant to use formal verification language: SPARK.