I found one of the comments made in passing to be very interesting.
Very very heavily paraphrasing:
>[Coq is useful in its way for providing proofs of termination of a partial function, but not really practical for most purposes in programming]
>[Proofs are not a first class object in Haskell (but are in Coq)]
Interested, I looked for what is out there on the web on this sort of thing:
* https://basics.sjtu.edu.cn/~yuxin/teaching/Coq/Coq2018.html, a 2018 course on coq
* https://coq.inria.fr/tutorial-nahas, a tutorial for using the language / getting started
* https://coq.inria.fr/, the main page for the language
* https://softwarefoundations.cis.upenn.edu/, some resources on proof systems
* http://adam.chlipala.net/itp/, older but still valuable resources on formal proof systems (2006)
Coq is not unique. For instance, the redprl project (a successor to nuprl, another proof system), can be found here http://www.redprl.org/en/latest/
Small proof languages can be thought of as a subset (subcategory?) of functional programming languages, and you can write things like web servers in them, eg https://github.com/coq-concurrency/pluto.