Víctor ( https://lopezjuan.com/ ) will do an introduction to dependently typed programming, in which you can guarantee that your program is correct before even running it!
PugglePay/Zimpler will sponsor pizzas as usual!
I will use the Agda language for the tutorial. Everything we'll see applies to any other functional language with dependent types (e.g. Idris).
Agda is almost always used from its (impressive) interactive emacs mode. Setup instructions @ http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Download .
(and, obligatory link: https://www.youtube.com/watch?v=oKUscEWPVAM )