Synthesis of list algorithms by mechanical proving

摘要

Program synthesis via extraction of programs from constructive proofs is now very well established, with a large literature base. There are still quite a few hurdles to overcome, but the meta-theory has been in place for quite some time now. It is thus disappointing that the authors of the paper seem to ignore almost all of it. Looking at their references, one is at once struck by how old most of them are; this is not necessarily bad-the pioneers deserve continued recognition. But this research area is currently extremely active, so it is baffling to find no reference to it at all. Especially since there really is a lot of relevant work around; various items done with Coq, Isabelle, or ACL2 come immediately to mind. Every proof strategy that I looked up was known or a special case of a strategy in Visser's 2005 survey. Automating such proofs is now considered feasible; see Claesen and colleagues for just one example.