> I do not see how you can reason about Haskell in Haskell either, as this is a programming language and not a proof language (maybe I am missing something?).

> I do not see how you can reason about Haskell in Haskell either, as this is a programming language and not a proof language (maybe I am missing something?). http://www.haskellforall.com/2013/12/equational-reasoning.html http://www.haskellforall.com/2013/12/equational-reasoning.ht... http://www.haskellforall.com/2014/07/equational-reasoning-at-scale.html http://www.haskellforall.com/2014/07/equational-reasoning-at... The reasoning is entirely carried out by replacing Haskell expressions with contextually equivalent ones. > Since with both Haskell and JavaScript you will need to define a propositional equality No, you need much more than a propositional equality to be able to reason about JavaScript programs. If you try to use Haskell-style equational reasoning on JavaScript objects, you can only pick between your reasoning being trivial (because every object reference is only equal to references to physically the same object) or unsound! So if you want a more useful notion of program equivalence, you'll have to use a separate logic (e.g. Hoare logic) or axiomatic system (e.g. Dijkstra's predicate transformer semantics) for reasoning about imperative programs.