A gentle introduction to functional programming with dependent types.
Dependent types enhance precision and safety of programs, allowing programmers to design software with higher assurance guarantees.
Various interesting examples will be presented to illustrate the use of Dependent Type Theory, using the Lean4 programming language and theorem prover.
Lean4 has some nice features like interactive evaluation, compilation to native code, and while so far mostly being used to formalize mathematics it is also a formidable modern elegant programming language.