Coq and other trustworthy proof assistants such as Isabelle/HOL are seeing increased use in construction of large software systems with accompanying machine-checked correctness proofs - paradigmatic examples include the CompCert verified C compiler and the seL4 verified operating system kernel. The field in computer science concerned with such applications (overlapping heavily with formal mathematics) is usually called proof engineering.
We are happy to announce the publication (on September 3, 2019) of an extensive survey of the scientific literature on proof engineering for software systems using proof assistants:
Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. QED at Large: A Survey of Engineering of Formally Verified Software. Foundations and Trends in Programming Languages (FTPL), Vol. 5: No. 2-3, pp 102-281, September 2019.
Note that the pdf is available for free download until around September 10, 2019.
Most of the authors are Coq users, and we believe the survey can be useful to the Coq community, both as a distillation of existing knowledge and for its comparisons with other proof assistants.
If you find any errors not already documented in our errata, please report them as a GitHub issue or pull request for the errata source file, or by contacting us directly.
The small verified regular expression matcher Coq project used as a motivating example in chapter 2 of the paper is available on GitHub.