Comment by 6gvONxR4sf7o

Huh, I wasn't actually going for snark. I was trying to preemptively be over-specific about what I meant. As in, you said "... writing the correct program..." and I meant that I'm talking in terms where functions are equal or distinct only based on extensional equality and with some flexibility on computational interpretation and axioms of the logic.

Like, if you meant "the correct program" in a sense where two pure total functions can be different despite both having the same outputs on the same inputs, then that's not what I'm responding to.

And yeah I know prolog, but proof assistants and logic programming are totally different beasts. Definitely not copy/pastable to/from lean, at least as I've seen and used each.

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

I think you're totally misunderstanding. What I'm saying is that in something like Lean (just because I know it best) I can say, "this function takes inputs satisfying Prop1 and returns outputs satisfying Prop2," in ways where I write some brute-force equivalent formalization of Prop1 and Prop2 in the most straightforward way, and then go on to prove that they are true of my program that is not the brute force implementation. Like the wacky famous magical inverse square root implementation from Quake III. You could write a spec that "output = 1/sqrt(input) up to float properties" and the implementation in the famous brainfuckery way. To your comment about how the spec is as hard as the implementation, "output = 1/sqrt(input)" is way easier than the weird efficient implementation, and that class of distinction is super common.

And as you said, the annoying part is showing that the efficient implementation satisfies the spec, but what's magic today is that we have great tools and LLMs can and do fill in the blanks. In practice, I write the spec by hand for the stuff I care about and then prompt the rest and know that my spec is what the LLM implemented.

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

I tried rocq back when it was coq too, and now do most of my work in lean and rust and python with totally normal folks and I'm convinced that the tooling and languages are finally just about Good Enough. If you have any interest in the field, which it sounds like you do, and if you haven't checked out the ecosystem in the last couple years, I'd recommend you check it out again.