Wednesday, March 19, 2014

r = maths : types : proofs : goals : r

Remember the first time when a certain math teachers asked us to chain theorems for a proof. A trick he told us was not to try to go from A to Z but try to imagine what Y could be. Sometimes thinking from the goal gives you insights and will help lead the other side of the chain.

In college 5th year, we try to apply typed logic to programs, especially when designing recursive function which can be hard to comprehend fully. A similar trick was used, the function will use its own end goal to feed itself. So taking into the result type into account helps you framing what each recursive case should do.

That's all folks, flash-un-news of the moment I needed to write down.

No comments:

Post a Comment