Rubrication

Standard functional programming languages like Haskell and SML use polymorphic type systems. These type systems however, are not sound. What this means is that the type-systems themselves can not be used to prove properties of the software in the sense of "total correctness". To see that this is true, we can get a "proof" (read program) of inhabitation of any arbitrary type A, by simply using the program: data Bot {- Look Ma! No constructors! -} bot :: Bot bot = bot Clearly when we say that bot is an inhabitant of Bot, we dont mean that it actually produces a value of type Bot, since there aren't any as Bot has no constructors! We can easily use this type of proof to prove something like A ∧ ¬ A which leads to a pretty degenerate logic. However, the type system is still *useful* in the sense that if the program ever *does* terminate, it's sure to do so with the appropriate type. This means we can get the full class of Turing complete programs, a...