The files Preface.v and Postscript.v from the old SF can be found in the /old directory. They should be translated to Lean/Verso format, moved into the LF directory, and added to the list of "finished" files that get included in the public-facing versions of LF.
One bit that should be added to the preface (and improved / extended):
Why SF-in-Lean? There are excellent texts on both
[programming](https://lean-lang.org/functional_programming_in_lean/) and
[theorem proving](https://lean-lang.org/theorem_proving_in_lean4/) in Lean. The
[How to Prove It! in Lean](https://djvelleman.github.io/HTPIwL/) book introduces
logic and proofs in Lean.
The files
Preface.vandPostscript.vfrom the old SF can be found in the/olddirectory. They should be translated to Lean/Verso format, moved into the LF directory, and added to the list of "finished" files that get included in the public-facing versions of LF.One bit that should be added to the preface (and improved / extended):