Comment by cayley_graph

> I’m not even going to get into how you could provably transform brute force propositional logic into efficient algorithms.

> The entire problem is showing that an efficient/reliable program actually implements those rules.

Reliability is a standard matter of correctness and captured (partly) by specifications. Efficiency tends to be easy to empirically test, but it is also possible to capture at the specification level [1]. Mind that specifications need not be all-consuming.

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

Agree! But this stuff just got massively more accessible, and the tooling around it is growing quickly. I think we'll end up growing specification systems specific to various domains which will be palatable to those "systems engineers", but I err on the side of optimism here. There's definitely a lot left to do for practicality.

[1] See the work of https://cs.nyu.edu/~shw8119 for the case of provably-efficient parallelism and garbage collectors