1. 4
  1.  

  2. 2

    This article has many problems but I’ll pick on what I think is the most interesting one:

    Sadly, type systems fundamentally can’t catch all kinds of programming mistakes, nor will they magically improve the time or space complexity of your algorithms.

    We can actually ensure that our algorithms have the correct complexity!

    http://twanvl.nl/blog/agda/sorting