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 pull: Huge motivation for the funding and introduction of formal methods for chip development.

Types

HOL/Isabelle

HOL Interactive Theorem Prover

Coq (+ Cedille, + LTAC, …)

Coq is a theorem prover that uses principles from type theory to provide formalizations of programs.

Libraries

Logitext: 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 A formally verified high-level synthesis tool based on CompCert and written in Coq cs guy working on certicoq A collection of tools for writing technical documents that mix Coq code and prose. Coq to Cedille compiler written in Coq An axiom-free formalization of category theory in Coq for personal study and practical work Software Foundations https://github.com/hwayne/lets-prove-leftpad "Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2020" https://github.com/achlipala/frapapp formal reasoning about programs website denotational semantics of imperative language in the style of software foundations https://github.com/uwplse/pumpkin-pi something to do with a coq plugin suite? verifcomp 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: a textbook for learning more coq! Coq proofs for the informal programmer, supposedly http://web.mit.edu/cpitcla/www/coq-rst/universe-polymorphism.html

Resources

Software Foundations: Learn about the foundations of software through exploring the proof assistant, Coq. Introduction to Homotopy Type Theory and Univalent Foundations (HoTT/UF) with… "A Little Taste of Dependent Types" by David Christiansen - YouTube: Goes along with the "little typer" book! My hobby: proof engineering | Stephan Boyer: 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.