I interactively build a simple B-tree data structure in Haskell, implementing insertion and deletion, using a GADT to enforce the structural invariant. The GADT also guides us towards a correct implementation.
You can download the video as MP4 or WebM, as well as the slides I used for my YLJ13 talk, in PDF or Keynote. There’s some code on GitHub. Sorry, no subtitles yet, but you can read along with this script. Also on YouTube.