The idea of computable reals go back to at least Turing. The idea is that a real number (or an operation on real numbers) is computable if we can compute the de

The idea of computable reals go back to at least Turing. The idea is that a real number (or an operation on real numbers) is computable if we can compute the decimal digits, one by one. This way, if the user wants to know it to any desired precision, they just have to wait until the computer has printed that many decimals. You can equivalently treat them as terminating computable functions of type (nat -> bool), which computes the n:th binary decimal. This is actually a quite constructive notion! At least, it works well with intuinistic mathematics, which is why Andrej Bauer is writing about it.