A book on Lean 4 as a programming language (rather than as a theorem prover).