Theorem provers are automated or semi-automated tools for composingproofs about statements or programs, allowing one to express theirthoughts

https://github.com/hwayne/awesome-cold-showers: It's one of thebiggest one of these…

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

Types

HOL/Isabelle

HOL Interactive Theorem Prover

Coq (+ Cedille, + LTAC, …)

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

Libraries

Logitext: A theorem prover built onHaskell and Ur/Web. Worth reading and learning about - or at leastinspecting the source code. Not sure if UrWeb is worth it but it looksfun to poke around with. https://github.com/DeepSpec/InteractionTreesa neat representation of recursive and impure Coq programshttps://github.com/mattam82/Coq-Equations function definitions for Coqhttps://github.com/MetaCoq/metacoq metaprogramming

References

https://github.com/atharvashukla/coq-tactics-index index of coqtactics and their meanings https://github.com/UniMath/UniMath coq andmath? https://github.com/codyroux/name-the-biggest-number proving thebiggest number in coq constructivelydmelcer9/coq-lunch-learnA formally verified high-level synthesis tool based on CompCert andwritten inCoqcs guy working on certicoq Acollection of tools for writing technical documents that mix Coq codeand prose. Coq to Cedillecompiler written in Coq Anaxiom-free formalization of category theory in Coq for personal studyand practical workSoftware Foundationshttps://github.com/hwayne/lets-prove-leftpad "Problem Sets for MIT6.822 Formal Reasoning About Programs, Spring2020"https://github.com/achlipala/frapapp formal reasoning about programswebsite denotational semantics of imperativelanguage in the styleof software foundations https://github.com/uwplse/pumpkin-pi somethingto do with a coq plugin suite? verifcomphttps://www.reddit.com/r/Coq/comments/tzpb9/webbased_proofbypointing_frontend_to_coq/https://news.ycombinator.com/item?id=26288749: a great approach to coqthrough a sample z3 tutorialcoqart:a textbook for learning more coq! Coq proofs for the informalprogrammer, supposedlyhttp://web.mit.edu/cpitcla/www/coq-rst/universe-polymorphism.html

Resources

Software Foundations:Learn about the foundations of software through exploring the proofassistant, Coq. Introduction to Homotopy Type Theory and UnivalentFoundations (HoTT/UF)with…"A Little Taste of Dependent Types" by David Christiansen -YouTube: Goesalong with the "little typer" book! My hobby: proof engineering \|StephanBoyer:A writeup from an AirBnB software engineer about proving things in Coqfor fun; this helps Stephan explore ideas and justify ides in types,logic, and algorithms; proving ideas is a tool for thinking about them.