Jon Pretty

Here's a crazy idea: the Void type in Haskell represent False in logic, but it's not empty--it contains bottom, which is a never ending computation. So we cannot prove False in finite time. But if we fall into the black hole, we'll see the proof of False when crossing the horizon