1 files changed, 36 insertions, 0 deletions
diff --git a/microposts/why-software-foundations.org b/microposts/why-software-foundations.org
new file mode 100644
index 0000000..6f8257a
--- /dev/null
+++ b/microposts/why-software-foundations.org
@@ -0,0 +1,36 @@
+#+title: Why you should read Software Foundations
+
+#+date: <2022-01-13>
+
+I finished reading the [[https://softwarefoundations.cis.upenn.edu/lf-current/index.html][Logical Foundations]], the first volume of
+[[https://softwarefoundations.cis.upenn.edu/][Software Foundations]].  What an amazing book.
+
+I learned about formal proofs before, by playing the [[https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/][natural number game]]
+designed by Kevin Buzzard, which is in Lean.
+
+Logical Foundations covers all that and goes much deeper.
+
+There are many great things about this book.  You can download it,
+ignore the html files, and just burn through the coq .v files, which
+are actually the source of the webpages.  The texts are basically
+comments in the .v files, but the readability is not worse than the
+html files, and actually much better in emacs.  It is almost like
+literate programming.
+
+As an aside, initially I had some problems with getting org-babel to
+work, but the files were deleted years ago.  After reading LF I
+realised org-babel is not really important, since I can just happily
+work through the giant .v files in [[https://proofgeneral.github.io/][Proof General]] (which you can
+easily install manually without MELPA).
+
+Another neat thing about LF is that it really demonstrates the
+parallel between propositions and types, by using the same arrow
+notations for implication and function, by making no notational
+distinctions with proofs of a theorem and elements of type.  A Proof
+is a Definition, and a property of numbers is a dependent type.  If
+you want to understand Curry-Howard Correspondence, you can't go wrong
+with Logical Foundations.
+
+By the end of book, you will have worked through the implementation of
+a mini imperative language called Imp, and proved some simple
+properties of programs written in Imp - great value for your time!