[rtpg]

My belief is that the core part of a lot of programs where you want formal proofs are tricky enough to where you need hand holding but the higher up the stack you go the simpler your proofs get since you did the hard stuff in the core.

Though it really does feel like we're still scratching the surface of proof writing practices. A lot of proofs I've seen seem to rely only on very low level building blocks, but stronger practitioners more immediately grab tools that make stuff simpler.

I would say, though, that it feels likely that your proofs are always going to be at least within an order of magnitude of your code, because in theory the longer your code is the more decision points there are to bring up in your proof as well. Though automatic proof searches might play out well for you on simpler proofs.

[tsimionescu]

> My belief is that the core part of a lot of programs where you want formal proofs are tricky enough to where you need hand holding but the higher up the stack you go the simpler your proofs get since you did the hard stuff in the core.

I don't think this is true at all. For many kinds of programs that it would be good to have formal verification for, all of the details are very important. For example, I'd love to know that the PET scan code was formally verified, and that it's impossible to, say, show a different radiation dose on the screen than the dose configured in the core. I very much doubt that it's easy to write a proof that the GUI controls are displaying the correct characters from a font, though.

Or, it would be good to know that the business flows in the company ERP are formally verified to actually implement the intended business processes, but even the formal specification for the business processes in a regular large company would likely take longer to produce than it takes for those same business processes or external laws to change.