Umm... just pointing this out because I'm from the Programming Languages side of things, but there are such things as total programming languages in which all functions must provably terminate before the compiler/type-checker accepts them.
I can imagine a learning framework built around learning total functions over codata.