ML for the working programmer

What Hacker News says

1. i_don_t_knowMay 2024
   See also “Designing a Theorem Prover” https://arxiv.org/pdf/cs/9301110

   And chapter 10 of ML for the working programmer, freely available at https://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html

   thread
2. PenyngtonFeb 2023
   SML is probably my favourite programming language, and ML for the Working Programmer is probably my favourite programming book. It is indeed sad to think that I'll probably never use it seriously or even meet another SML programmer in my life (I met one at university in a larger city once, but it seems unlikely to happen again where I am now).

   OCaml is good, though I personally dislike its complexity compared to SML ("Perfection is achieved, not when there is nothing more to add, but when there is nothing left to take away." and all that). There are also remote OCaml jobs in the world, so it's not completely impossible I could do something like that in the future.

   Show morethread
3. cannamOct 2022
   > By the way, wasn't there a "ML for the Working Programmer" aeons ago?

   There was. It was written by the author of this very submission and you can download it free from his site (follow the link trail from author's name at the bottom of the article). Great book, a real favourite, though I'm not sure it totally captures the anxiety-driven copy-paste frenzy of the true working programmer.

   There is one SML compiler that has an extremely cute logo - SML# (https://smlsharp.github.io/en/)

   Show morethread
4. taconMar 2021
   ML for the Working Programmer

   https://www.cl.cam.ac.uk/~lp15/MLbook/

   thread
5. nextosNov 2020
   A similar book to Concrete Semantics, which I love, is Formal Reasoning about Programs by the same group the OP link comes from: http://adam.chlipala.net/frap/frap_book.pdf

   ML for the Working Programmer is written by Paulson, one of the main persons behind Isabelle, and ends up with a prover project: https://www.cl.cam.ac.uk/~lp15/MLbook/

   Paulson teaches an undergrad course in Cambridge which is now using Huth & Ryan as a textbook. It's an incredible book that focuses on logic, SAT solvers and model checking. Probably the place to begin. An incomplete draft 2nd edition is in the authors website: ftp://ftp.cs.bham.ac.uk/pub/authors/M.D.Ryan/tmp/Anongporn/Ch1+3.pdf

   If you are interested in tableaux techniques, First-order Logic and Automated Theorem Proving by Fitting is a good text.

   Personally, I think the place to start from is Huth & Ryan. Logic is the calculus of CS. Then progress to type theory using a book like TAPL by Pierce or Proofs and Types by Girard.

   Then, depending on your interests, you can proceed to model checking, program analysis and theorem proving. For the first two, the classics are Katoen and Nielson & Nielson, respectively.

   Show morethread
6. bachmeierOct 2020
   ML for the Working Programmer is an awesome textbook to use to learn programming. It is free to download on the author's website:

   https://www.cl.cam.ac.uk/~lp15/MLbook/pub-details.html

   thread