Yes! Dafny puts this stuff front and center, it's all well and good to think about invariants, but if they're just expressed in a comment and not actually veri

Yes! Dafny puts this stuff front and center, it's all well and good to think about invariants, but if they're just expressed in a comment and not actually verified, they might as well be filler text! If there's anything I hope the mainstream adopts at some point, it is some variation of what Dafny offers here.