This workshop provides 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 & monads, and while so far mostly being used to formalize mathematics and for software verification, it is also an elegant modern powerful SOTA general-purpose functional 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)

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 want to use a different editor/IDE on Fedora or EPEL, I suggest to use my Copr repo https://copr.fedorainfracloud.org/coprs/petersen/lean4/ (note the current 4.20.0 builds are actually 4.20.1). Note if your editor does not support LSP you will be at a severe disadvantage, since interactivity/feedback is essential for Lean.

You can also use the Lean version manager called Elan to get lean4 (and this is what the vscode extension does), but note 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 alright too. For Emacs you will also want to install lean4-mode and lsp-mode if you don't have them already.

I will be using the latest lean4 version 4.20.1, though any recent release (from say this year) which works should be fine too: do test your installation beforehand to confirm your setup is okay: see the readme in the github repo.

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

More info

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