Introduction

• Lean is a new(ish) programming language
  • Pure: functions always return the same output for the same input
  • No mutable state: cannot modify data structures in place (create new ones)
  • Side effects (like I/O) are tracked by the type system
• See [Christiansen2023] for reference

Tooling

• Don't normally recommend specific editors…
• …but Lean has committed heavily to language servers
• These lessons were written using VS Code