[Gajurgensen]

Program synthesis is of course very difficult in general, especially if you want it to be entirely automated. One option to make it more practical is to have the user drive synthesis from specification to implementation via something which looks like a sequence of tactics.

(I'll add a plug to some stuff we are working on at Kestrel: https://www.cs.utexas.edu/~moore/acl2/manuals/latest/index.h.... We've used the APT library to do stepwise refinements from specs ACL2 to C code. Each step is something like "make function tail recursive" or "switch to a new, isomorphic shape of the data").

By the way, Curry-Howard offers a compelling insight here: deriving programs from specifications (i.e. types+propositions) may be the same process as deriving proofs from propositions. So the two processes can in principle work the exact same way.