I think it is very counterintuitive---even to professional programmers---that you can compute things without letting the computer know them. I literally had to go through the entire paper to understand that this can actually work as long as human in the loop doesn't screw up (see my summary [1], which was revised multiple times at that time).

[1] https://news.ycombinator.com/item?id=28223141