1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
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!
|
