I wouldn’t call them worthless. I guess it depends on the unit. But also having someone or something independently write tests is generally better than testing your own code.
How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.
I was going through an experiment trying to spec out a simple caching system in Lean. I was getting Gemini to help me run through doing this, step by step. At one point it writes out this statement with a proof to show something, the specifics of which I forget, but it was some simple property of the cache. I stare at it for a while thinking to myself this can't be right, it was some sort of plain tautological statement that didn't really say anything, like saying 1 = 1.
I give it to Opus 5.5 and it basically confirmed my gut feeling that it was useless.
I'd like to rely more on formal verification. I like the idea of starting out with specs in a formal setting and designing software that way. The problem is it's hard to do right, and my point is even with AI, it's hard to do right.
I fully agree it’s harder to read. I do chip design and I feel like formal is more common in this area, but I generally restrict it to very simple properties that are easy to understand without having to mentally solve a sudoku puzzle.
It’s to easy to write an assertion that looks like it checks what you want it to, and gives you a false confidence when it passes, only to figure out after a field failure that it wasn’t checking what you thought at all.
But I’d pay for a commercial set of properties and assertions that had guarantees, and not worry about their complexity. For something standard like cache protocols and bus protocols.
Other cases it needs to be pretty straightforward to grasp by a peer reviewer in minutes, or it’s not worth it.
But when you can hit the sweet spot, a set of easily understood properties (or complex but trusted properties), formal can save massive amounts of time.
That's the nice thing about the approach described in the blog: you use the same Rocq theorem for every binary (it just says "this binary doesn't crash") and then you express the property you want in your language of choice. For example, to prove that your compression algorithm round-trips, you would write something like assert(x == decompress(compress(x))).
You do it by comparing to something that is “known” to be good.
I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.
Proving two things are equivalent is a major component of formal.
For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.
A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.
> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.
> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.
- - -
This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.
If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.
One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people
Nobody (sane) does that.
Lots of people have the implementer write the tests. But this only seems like a bad thing because of an unfortunate terminology collision:
- Microsoft culture: tests are adversarial verification.
- Google culture: tests are executable documentation.
Both of these things are important. It's really unfortunate we call both of them "tests".
At Microsoft, (verification) tests are written by a different engineer than the one who wrote the code under test. VLSI/Hardware works like this too.
At Google, (documentation) tests are written by the person who wrote the code, because it's their job to document it, and because the point of documentation-tests is to make sure other people who modify your code don't break it.
The memory constraint isn’t design. It’s fab capacity. Apple has exactly 0 fabs. By the time they hired domain experts and built fabs and tuned to the point of reasonable yields, the crunch would have been over for 5 years, and apple would have wasted 20 billion with no return.
The fact that you can significantly alter the trajectory of an object by ejecting mass is well understood. That's pretty basic physics. If you want to call this flying you're going to have to explain how you propose to do it for long enough that you can do it outside of a controlled - and quite possibly rigged - demo.
Satellites are on a ballistic trajectory, they don't 'hover' but they will stay aloft long enough to be useful. A bullet fired horizontally is going to follow a parabola and then impact (the ground or something else) it does not hover. A car that is dropped that ejects a significant fraction of its mass in any direction is going to alter its trajectory but that won't change much: it's going to come down, and sooner rather than later, it isn't 'hovering' it is just very temporarily staving off the inevitable.
If you show me this car staying in place for more than a couple of seconds I would agree it is hovering, the mass ejection trick would have to be replaced by something that actually works. But this is just a gimmick: it gives the illusion of a hover by ejecting a bunch of mass so large that outside of a split second demo it isn't going to work, it's going to come down within a very short time and there is nothing that will stave that off.
>A car that is dropped that ejects a significant fraction of its mass in any direction is going to alter its trajectory but that won't change much: it's going to come down, and sooner rather than later, it isn't 'hovering' it is just very temporarily staving off the inevitable.
People are under helicopters all the time. SAR for instance. So whether you are supposed or not doesn't matter, for some people that's their day job and they are not overly worried that it is going to fall on them because they know it can hover.
reply