alt Hacker News> 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.
> 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.