"Wadler created ML to help automate proofs". Minor nitpick: actually, ML was designed by Robin Milner: http://en.wikipedia.org/wiki/ML_(programming_language)