Your last point is interesting - I believe Idris and/or Agda in fact go out of their way to show a natural number type defined using induction as a key example.

Your last point is interesting - I believe Idris and/or Agda in fact go out of their way to show a natural number type defined using induction as a key example. I remember being blown away by that. Coming from dynamic languages towards appreciation of static types, this sort of thing is inspiring. I've been looking forward to writing some practical work in those languages when children and time give the chance.