Too bad the article didn't go all the way into computation-land, so I can't readily believe the "finitariness" of the insights contained there. For example, is

Too bad the article didn't go all the way into computation-land, so I can't readily believe the "finitariness" of the insights contained there. For example, is the function E() actually implementable in Haskell? If it isn't, the whole premise kind of collapses... One way to make sense of this question would be to skip the red herring of constructibility and define reals as lazy streams of bits, then try to write actual code and stuff. (But how in the flying hell do you implement a rationality predicate on reals-as-streams?) There are probably other, non-equivalent ways. This stuff isn't trivial at all. For a more enlightening perspective on such topics, see the blog "Mathematics and Computation", especially those articles: http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/ http://math.andrej.com/2007/09/28/seemingly-impossible-funct... http://math.andrej.com/2008/02/06/representations-of-uncomputable-and-uncountable-sets/ http://math.andrej.com/2008/02/06/representations-of-uncompu...