> 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.