But assuming "if we knew what computers do, we would not use them" is true, then the rest of his talk is pointless.
We use computers precisely because we know what they do. We're worried about black boxes and long for formal proofs of our programs because they are useful only when we know what they do.
If I hand you a black box with a button and two LEDs that blink in response to input, it would be initially useless to you precisely because you do not know what it does. Only if you learn what it does, by exploration or me telling you, can it become useful to you.
I think that an overly literal and precise reading of his pithy phrase misses the point.
Computers do exactly as we tell them to do, and we might also know what we'd like them to do but we usually don't know what we'd like about the result of what they do. Since the birth of computer science we've known that computers are mysterious in the sense that even though their operation is deterministic in a very natural sense, its outcome is not generally knowable; so deterministic but indeterminable. Dowek merely points out that this is not just a problem with computers but also the very point of them. If their operation's outcome were easily determinable, we wouldn't need it.
> I think that an overly literal and precise reading of his pithy phrase misses the point.
I suppose you're right. I get what you're saying, and based on that it seems what Dowek should have said was that "if we knew what computers would do, we would not use them".
For me that's a pretty crucial distinction though.
In any case, I agree that computation being deterministic yet indeterminable is indeed fairly surprising[1] and quite interesting, and indeed it is this potential for complexity that makes computers useful.
Surprise in this context means you didn't know the exact data the computer will output, not that you don't know how a computer or the program works.
Like if you ask a calculator to calculate sin(13), you know exactly how it calculates it but you didn't know the exact number so the result was "surprising".
We use computers precisely because we know what they do. We're worried about black boxes and long for formal proofs of our programs because they are useful only when we know what they do.
If I hand you a black box with a button and two LEDs that blink in response to input, it would be initially useless to you precisely because you do not know what it does. Only if you learn what it does, by exploration or me telling you, can it become useful to you.