Not every program property of interest can be (conveniently) verified using automated tools - especially if your verification tool is a type checker! Sometimes

Not every program property of interest can be (conveniently) verified using automated tools - especially if your verification tool is a type checker! Sometimes you need to roll up your sleeves and prove things yourself. (Which, by the way, isn't always a bad thing.) That being said, hopefully you won't have to use set theory, where any structure that actually matters to you has to be encoded in terms of sets containing sets containing sets, until you reach turtles.