Learning Agda has quite an academic feeling to it, not because it's not widely used, but because the ressources are so scattered around, often out of scope for beginners, and so on.

For that reason, I really appreciate these "let's do a simple task with no prerequisites" kind of posts about it. It shows me (and probably many other Haskellers, functional programmers, programmers) that simple problems are manageable, and provide plenty of catchwords to read up on. Thanks for that!