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.

You are viewing proxied material from sdf.org. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.