I have the impression that for someone coming from a programming background, Idris is also a pretty good introduction to the world of dependently typed programming and proof assistants.