Yeah, the domain name is misleading. It really should be called "Equational reasoning for all". I'm reluctant to change it at this point, but I think I should

Yeah, the domain name is misleading. It really should be called "Equational reasoning for all". I'm reluctant to change it at this point, but I think I should make more of an effort to clarify that the posts are advocacy for purely functional programming languages, including Idris in particular since it is maturing quite rapidly. Tonight I will revise this post to be less Haskell-centric by mentioning that most of what it describes applies to other purely functional languages and also mention how dependently typed languages can improve and mechanically check the proof process.