I think we're in agreement. My comment about the halting problem was meant to refer to Rice's theorem (the name was slipping my mind), which I occasionally see people use to justify the idea that you can't prove interesting facts about real-world programs. In practice, real-world programming involves constantly proving small, useful theorems. Your useful theorem (e.g. `Map[User,Seq[Account]] => Map[User,NetWorth]`) is probably not that interesting to even the category theorists, but that's fine, and there's plenty you can learn from the theorists about how to factor the proof well (e.g. as _.map(_.map(_.balance).sum)).