[EGreg]

It seems to me that we should have a different measure than lebesgue measure when we speak of picking numbers from an interval.

I wonder if there is a measure under which computable numbers have measure 1 while the others have measure 0. Would it have all the correct properties?

[man-and-laptop]

That's not necessary with Type 2 Theory. You work with the usual set of real numbers.