[IngoBlechschmid]

Indeed, what you write is true from an external point of view; just note that within this flavor of constructive mathematics, the set of functions from N to Bool is uncountable again.

There is no paradox: Externally, there is an enumeration of all computable functions N -> Bool, but no such enumeration is computable.

[skissane]

Is it internally uncountable in the strong sense that the system can actually prove the theorem “this set is uncountable”, or only in the weaker sense that it can’t prove the theorem “this set is countable”, but can’t prove its negation either?

If the latter, what happens if you add to it the (admittedly non-constructive) axiom that the set in question is countable?

[btilly]

It should be true in the stronger sense.

Suppose that you've written down a function enumerate, that maps all natural numbers to functions that themselves map all natural numbers to booleans. We then can write down the following program.

    (defn unenumerated (n) (not ((enumerate n) n)))

This function can be recognized as Cantor diagonalization, written out as a program.

If enumerate actually works as advertised, then it can't ever find unenumerated. Because if (enumerate N) is unenumerated, then ((enumerate N) N) will hit infinite recursion and therefore doesn't return a boolean.

This argument is, of course, just Cantor's diagonalization argument. From an enumeration, it produces something that can't be in that enumeration.