Am working on rewriting an imperative programming course to use Dafny to present verified algorithms and data structures.