Book Review
Program = Proof by Samuel Mimram: Part I
LdBeth
Well, I once became a big fan of programming with
dependent types. However since I'm the determined LISP fan
and will be always the lisp fan, and most of the time I
write program for retro platforms, I think it is far from
possible to compile anything like Haskell or Rust to my
pocket calculator for example, so I gave up on these shining
but heavy to setup stuff.
However, since this book has been staying in my list
for long, I should finish reading it so I can say good bye
to type theory, at least temporarily, until one day it gets
more useful.
First, a little bit 1. Beginning of the book
about me, if you do not know
me well. I am the freelance OK, let's get into to
lisp programmer. I do not the topic. I skipped mostly
treat programming as a pro‐ first part of the book,
fession, although I learned since it is about OCaml. If
programming for fun. So you ask me what I think
don't treat me like anyone about OCaml, I would respond
expert in computer science, so: "not as useful as lisp."
as I am usually biased to It is worth to notice that
hate very new stuff. the first chapter introduced
the empty type pattern:
I have seen people
(younger than me) who type empty = |
started from a teenager
hacker and got involved into Which really does not
homotopy type theory a lot. have other use than define
Soon they started to talk the empty type.
about kan operator, pullout,
cubic, stuff that I can not The typing rule seems
understand. However, believe very confusing to beginners
me that if you just wants to of types, well, it is only
be a programmer, and write because one does not have no
assembly for HP Saturn or enough experience with any
M68k, these things are not of the typed programming
important at all. languages, otherwise it is
very ordinary.
A good book to refer‐ There are about several
ence on programming language proof searching strategies
and logic is Practical Foun‐ in Chapter 2 but I'm not
dations for Programming very into reading them,
Languages of Robert Harper. sorry about that.
2. Logic, logic, and more 2.1. Cut elimination
logic
While people mention
Unfortunately this is cut elimination, especially
not fully a programming in a constructive logic con‐
book. Well if you already text, it means the generated
know some propositional program from proof that
logic then this part should calls other programs
be easy. Yes the semantics (resulted from using lemmas)
is just boolean logic and can have these programs
one can brutal force, how‐ inlined.
ever not many real sized
problems can be brutal So, a constructive cut
forced but you get SAT elimination proof is essen‐
solver for these. tially an inline algorithm
for high level programs.
Maybe you could wait
for Donald Knuth's book on 2.2. Normalization by
SAT solver? I think the pre‐ evaluation
prints are already avail‐
able. Another glossary term.
It is really using the
Section 2.2.2 mentioned lambda constructs from the
an interesting graphic host programming language to
representation of FOL by exploit the optimization
Frege. The inference rules provided by the host com‐
might seem scary, but as I piler. If the host language
said one needs practice and itself is implemented in a
practice so familiarity can naive way then it would
be acquired. still suck.
Pretty much all proofs
involved in these parts
needs induction. I have not
practiced the actually proof
of these logic systems in a
proof assistant because it
is not fun at all to do so.
This concludes the first part of the book review. I
hope you can enjoy reading it.