the last two chapters - on automatically proving programs correct, as well as deriving correct programs from definitions - were puzzling. Felt too academic and somewhat out of place in a book teaching a programming language.

This is interesting, because I had the same experience with ML for the Working Programmer; the last chapter (a theorem prover) seems to come out of nowhere and seems to have little to do with the “working programmer” (although I have more appreciation for it now than when I first encountered this book and thought it a bizarre choice).

For me it is not overly surprising that a book about a language which was built to make a theorem prover, authored by an author who is doing theorem proving would include a chapter about… theorem proving. In a similar manner how SICP uses Scheme to implement Scheme.

For sure. But the idea that “theorem proving” was for the “working programmer” seemed bizarre to me in the late 90s, and I think only added to ML’s reputation as an academic language not for serious work. Thankfully the latter idea is well refuted now, and the former is starting to have some currency.

This is interesting, because I had the same experience with ML for the Working Programmer; the last chapter (a theorem prover) seems to come out of nowhere and seems to have little to do with the “working programmer” (although I have more appreciation for it now than when I first encountered this book and thought it a bizarre choice).

For me it is not overly surprising that a book about a language which was built to make a theorem prover, authored by an author who is doing theorem proving would include a chapter about… theorem proving. In a similar manner how SICP uses Scheme to implement Scheme.

For sure. But the idea that “theorem proving” was for the “working programmer” seemed bizarre to me in the late 90s, and I think only added to ML’s reputation as an academic language not for serious work. Thankfully the latter idea is well refuted now, and the former is starting to have some currency.