There are some possible approaches to automate testing in modern Coq.
- Writing test scripts with Ltac. This is the approach described in http://adam.chlipala.net/cpdt/, which the author uses with great success in projects such as http://adam.chlipala.net/papers/BedrockPOPL15/. It can significantly reduce the amount of test code required, but requires good handling of Ltac's peculiarities and does not seem easy to debug.
- Automation based on canonical structures. This is the approach described in https://people.mpi-sws.org/~beta/lessadhoc/, and it is used in Mathcomp. It involves taking advantage of the Coq type inference mechanism to automatically run logical programs that search for certain types of test terms. It is described in that document as less ad-hoc than the Ltac-heavy approach, but not necessarily quicker, and may be more detailed due to the need to use the mechanism of canonical structures for something that was not designed directly. .
- Dependent types / equations. The complement of Equations (https://www.irif.fr/~sozeau//research/publications/drafts/Equations_Reloaded.pdf) seems to facilitate in Coq the same convenience when working with programs written in a dependent manner as a language like Agda or Idris. With this approach, the processor acts as a form of automation, and the amount of test code is reduced by having the algorithms create, manipulate and transmit the terms of the test directly.
There are also some modern developments that complement these.
- Ltac2. This is intended to be 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 document states that "Ltac2 is still in an active development phase, but the basics of the language have been established.Most of all, users are needed to polish the rough edges". If it is intended to be a replacement superior to Ltac, should it be considered in lieu of Ltac for new projects, since it is already ready for user testing?
- Metacoq This provides meta-programming functions that allow the development of higher-level tools, as described in https://www.irif.fr/~sozeau/research/publications/drafts/The_MetaCoq_Project.pdf, and presumably simplify the use of the test by reflection, Technique used in approaches based on both canonical and Ltac-heavy structures.
My question is, if I am starting a new project, what criteria should I use to determine which approach or combination of them to adopt? As a concrete example, imagine that I want to verify the easy-to-verify parts of a program that connects to a server through the Internet, downloads some data, processes the data in some way and then serves the processed data through TCP. By easy to verify I mean not verifying the TCP / HTTP stack, or trying from scratch to correct the known algorithms used in data processing. When I consider how I would structure this, it seems that the structure would be quite different depending on which of the previous approaches I used, and I lack the experience to make a judgment about which would produce the best result in terms of maximizing production. of verified code per unit of development time. What factors should require the use of canonical structures or equations instead of just a single Ltac?