Fast and Loose Reasoning is Morally Correct

Nils Anders Danielsson, Jeremy Gibbons, John Hughes and Patrik Jansson (2005). Fast and Loose Reasoning is Morally Correct.

We justify reasoning about non-total (partial) functional languages using methods seemingly only valid for total ones; this permits "fast and loose" reasoning without actually being loose...

Functional languages satisfy many pleasing equational laws, such as curry o uncurry = id, (fst x, snd x) = x and fst(x,y) = x and many others inspired by category theory. Such laws can be used to perform very pleasant proofs of program equality... There is just one problem. In real programming languages such as Haskell and ML, they do not hold.

However, not to worry: The authors show that if two closed terms have the same semantics for total functions, they have related semantics for partial functions.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Caveat

Apparently it's only morally correct if you don't look at bottoms. (ba-doom tish!)