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.

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.