Haskell for all: Equational reasoning

You may have heard that Haskell is "great for equational reasoning", but perhaps you didn't know precisely what that meant. This post will walk through an intermediate example of equational reasoning to show how you can interpret Haskell code by hand by applying substitutions as if your code were a mathematical expression. This process of interpreting code by substituting equals-for-equals is know

[ilyaletre]

やはり数学の証明と同じ技法でプログラムの正しさを保証できることがメリットだと考えていいのかな。substitutionでequalityを保証しながらより効率の良いプログラムが得られるのは良いかも。

[tsimo]

"There is no need for a separate formal model because the code is already written as a bunch of formal equations."