[redjamjar]

Yeah, SPARK/Ada is a comparable system to Dafny. I agree with that! Also, Frama-C and a bunch of other more esoteric research languages as well.