I am collecting some data on FP used to introduce programming
ie as a first course: http://blog.languager.org/2014/08/universities-starting-functional.html

Naturally the haskell link is the first:
http://www.haskell.org/haskellwiki/Haskell_in_education

I was just wondering if there are more extremal cases of this:
eg Are there any univs using Idris/Agda to *introduce* programming/math/proofs etc