Bottom is a member of every type, so all Haskell programs correspond to proofs of trivial propositions. Or that is my understanding anyway.
And something similar should be true for common imperative languages.
Not quite. Bottom as a member of every type means that you cannot trust my proof (x : A) without examining it and that your examination may be non-terminating. That said, it you examine a realizer and terminate then you have a genuine proof of a potentially non-trivial theorem.
The reason why most Haskell theorems are trivial is because lacking dependent types means that we cannot ask for interesting theorems. `3 :: Int` is a perfectly nice proof that "Integers exist" which is a little silly.
