3
$\begingroup$

There are a few possible approaches to proof automation in modern Coq.

  • Writing proof scripts with Ltac. This is the approach described in http://adam.chlipala.net/cpdt/, which the author uses to great effect in projects like http://adam.chlipala.net/papers/BedrockPOPL15/. It can significantly reduce the amount of proof code required, but requires a good handle on the quirks of Ltac and does not seem straightforward to debug.
  • Canonical-structures-based automation. This is the approach described in https://people.mpi-sws.org/~beta/lessadhoc/, and used in Mathcomp. It involves taking advantage of Coq's type inference mechanism to automatically execute logic programs that search for certain kinds of proof terms. It's described in that paper as less ad-hoc than the Ltac-heavy approach, but not necessarily faster, and can be more verbose due to needing to use the canonical structures mechanism for something it wasn't directly designed for.
  • Dependent types/Equations. The Equations plugin (https://www.irif.fr/~sozeau//research/publications/drafts/Equations_Reloaded.pdf) seems to faciliate in Coq the same convenience when working with dependently typed programs as a language like Agda or Idris. With this approach the elaborator acts as a form of automation, and the amount of proof code is reduced by having algorithms create, manipulate and pass around proof terms directly.

There are also some modern developments that complement these.

  • Ltac2. This is meant as a replacement for Ltac, with fewer quirks and potentially better performance, as described in https://popl19.sigplan.org/details/CoqPL-2019/8/Ltac2-Tactical-Warfare. The paper states that "Ltac2 is still in an active development phase, but the foundations of the language have been settled. More than anything, it is in need of users in order to polish the rough edges". If it is meant to be a superior replacement to Ltac, then should it be considered instead of Ltac for new projects, since it's already ready for user testing?
  • Metacoq. This provides metaprogramming features that allow the development of higher level tools, as described on https://www.irif.fr/~sozeau/research/publications/drafts/The_MetaCoq_Project.pdf, and presumably simplify the use of proof by reflection, a technique used in both canonical-structures-based an Ltac-heavy approaches.

My question is, if I'm starting a new project, what criteria should I use to determine which approach or combination thereof to adopt? As a concrete example, imagine I want to verify the easy-to-verify parts of a program that connects to a server over the internet, downloads some data, processes the data somehow, then serves the processed data over TCP. By easy-to-verify I mean not verifying the TCP/HTTP stack, or proving from scratch the correctness of well-known algorithms used in the data processing. When I consider how I'd structure this it seems like the structure would be quite different depending on which of the above approaches I used, and I lack the experience to make a judgement regarding which would produce the best result in terms of maximising the output of verified code per unit of development time. What factors should necessitate the use of canonical structures or Equations instead of just plain Ltac?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.