A gentle introduction to functional programming with dependent types.
Dependent types can enhance the 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 functional programming and dependent types, using the Lean4 programming language and theorem prover.
Lean4 has some nice features like interactive evaluation, compilation to native code & type classes, and while so far mostly being used to formalize mathematics and for software verification, it is also an elegant modern powerful SOTA general-purpose programming language.

No prior knowledge of dependent types is required, but some basic understanding of functional and typed programming would be helpful.

https://lean-lang.org/lean4/doc/
https://lean-lang.org/

Preparation

Please install Lean4 yourself ahead of the workshop and check it is working correctly, so you can follow along the interactive demo and try the short tutorial exercises:

https://github.com/juhp/lean4-devconf.cz-2025-ws (workshop code - coming soon!)

Note: lean4 is quite a large download (several hundred MB) , so you may not have the bandwidth at the venue.

The simplest way to get Lean4 up and running is via its VSCode extension (ext install leanprover.lean4). Though if you are using Fedora or EPEL and another IDE, I suggest to use my Copr repo https://copr.fedorainfracloud.org/coprs/petersen/lean4/ (note the 4.20.0-2 builds are actually 4.20.1).

You can also use the Lean version manager called Elan to get lean4 (and this also what the vscode extension does), but if you are not careful you can end up with multiple lean4 versions getting pulled down via projects.

See the official upstream setup instructions at https://lean-lang.org/documentation/setup/ for more details.

VSCode is the best supported IDE but Emacs and Neovim should also work okay, and possibly other editors with decent LSP support might be fine also.

I will be using the latest lean4 version 4.20.1, though any recent release (from say this year) which functions should be fine too: do try to do a "helloworld" test beforehand to confirm your setup is okay.

As a last resort there is also https://live.lean-lang.org/ but it does not really allow any IO.

More info

https://github.com/leanprover/lean4
https://lean-lang.org/functional_programming_in_lean/