Section 1.5: Datatypes and Patterns - Termination discussion

[mbravenboer]

Thanks a lot for the book. I've really enjoyed working through it so far and the quality is great.

I had a couple of things that slightly confused me, maybe this is useful to clarify in the text:

Unlike many languages, Lean ensures by default that every recursive function will eventually reach a base case. From a programming perspective, this rules out accidental infinite loops.

A consequence of this is that Lean will not accept a version of even that attempts to invoke itself recursively on the original number.

It was not clear to me immediately what this means. I assumed that Lean will somehow by default refuse to run a recursive function that is not proven to terminate. I tested this (VSCode), and it crashed the Lean language process, so it appears it did just run the function. I think it would help here to clarify what the purpose is of the termination checks (eg something about the value of the diagnostics, but that it does not prevent the function from running).

[mbravenboer]

I've progressed a bit more in the book, and the distinction is now more clear: when you run the program from the command-line with lean --run, it does indeed refuse to run (same for out-of-bounds errors). However, when you use it from VSCode with #eval it does crash the process (same for out-of-bounds). I'd expect readers to be using VSCode in Chapter one, so probably good to clarify? Or is it considered a bug in the VSCode language server for Lean?

[david-christiansen]

Thanks for the report! I'm busy with Lean Together this week, but in the near future I'll be taking another pass to fix issues with the book and I'll definitely take care of this one.