Theorem provers are automated or semi-automated tools for composing
proofs about statements or programs, allowing one to express their
thoughts

<https://github.com/hwayne/awesome-cold-showers>: It's one of the
biggest one of these…

<https://en.wikipedia.org/wiki/Pentium_FDIV_bug>: Huge motivation for
the funding and introduction of formal methods for chip development.

# Types

## HOL/Isabelle

[HOL Interactive Theorem Prover](https://hol-theorem-prover.org/)

## Coq (+ Cedille, + LTAC, …)

Coq is a [theorem prover](id:0999656e-5b44-455f-8c33-bd51b0365b6b) that
uses principles from type theory to provide formalizations of programs.

### Libraries

[Logitext](http://logitext.mit.edu/main): A theorem prover built on
Haskell and Ur/Web. Worth reading and learning about - or at least
inspecting the source code. Not sure if UrWeb is worth it but it looks
fun to poke around with. <https://github.com/DeepSpec/InteractionTrees>
a neat representation of recursive and impure Coq programs
<https://github.com/mattam82/Coq-Equations> function definitions for Coq
<https://github.com/MetaCoq/metacoq> metaprogramming

### References

<https://github.com/atharvashukla/coq-tactics-index> index of coq
tactics and their meanings <https://github.com/UniMath/UniMath> coq and
math? <https://github.com/codyroux/name-the-biggest-number> proving the
biggest number in coq constructively
[dmelcer9/coq-lunch-learn](https://github.com/dmelcer9/coq-lunch-learn)
[A formally verified high-level synthesis tool based on CompCert and
written in
Coq](https://reddit.com/r/ProgrammingLanguages/comments/hx442x/a_formally_verified_highlevel_synthesis_tool)
[cs guy working on certicoq](https://www.cs.princeton.edu/~ckorkut/) [A
collection of tools for writing technical documents that mix Coq code
and prose.](https://github.com/cpitclaudel/alectryon) [Coq to Cedille
compiler written in Coq](https://github.com/pedrotst/coquedille) [An
axiom-free formalization of category theory in Coq for personal study
and practical work](https://github.com/jwiegley/category-theory)
[Software Foundations](https://softwarefoundations.cis.upenn.edu)
<https://github.com/hwayne/lets-prove-leftpad> ["Problem Sets for MIT
6.822 Formal Reasoning About Programs, Spring
2020"](https://github.com/mit-frap/spring20)
<https://github.com/achlipala/frapapp> formal reasoning about programs
website [denotational semantics of imperative
language](https://github.com/bendy/DenotationalSemantics) in the style
of software foundations <https://github.com/uwplse/pumpkin-pi> something
to do with a coq plugin suite? [verifcomp](https://verifcomp.dbp.io/)
<https://www.reddit.com/r/Coq/comments/tzpb9/webbased_proofbypointing_frontend_to_coq/>
<https://news.ycombinator.com/item?id=26288749>: a great approach to coq
through a sample z3 tutorial
[coqart](http://www.cse.chalmers.se/research/group/logic/TypesSS05/resources/coq/CoqArt/):
a textbook for learning more coq! [Coq proofs for the informal
programmer, supposedly](https://www.youtube.com/watch?v=5e7UdWzITyQ&t=0)
<http://web.mit.edu/cpitcla/www/coq-rst/universe-polymorphism.html>

# Resources

[Software Foundations](https://softwarefoundations.cis.upenn.edu/):
Learn about the foundations of software through exploring the proof
assistant, Coq. [Introduction to Homotopy Type Theory and Univalent
Foundations (HoTT/UF)
with…](https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html)
["A Little Taste of Dependent Types" by David Christiansen -
YouTube](https://www.youtube.com/watch?app=desktop&v=VxINoKFm-S4): Goes
along with the "little typer" book! [My hobby: proof engineering \|
Stephan
Boyer](https://www.stephanboyer.com/post/134/my-hobby-proof-engineering):
A writeup from an AirBnB software engineer about proving things in Coq
for fun; this helps Stephan explore ideas and justify ides in types,
logic, and algorithms; proving ideas is a tool for thinking about them.