[IngoBlechschmid]

> It seems like quite a paradox to build something but to not know how it actually works and yet it works. This doesn't seem to happen very often in classical programming, does it?

I agree. Here is a remote example where it exceptionally does, but it is mostly practically irrelevant:

In mathematics, we distinguish between "constructive" and "nonconstructive" proofs. Intertwined with logical arguments, constructive proofs contain an algorithm for witnessing the claim. Nonconstructive proofs do not. Nonconstructive proofs instead merely establish that it is impossible for the claim to be false.

For instance, the following proof of the claim that beyond every number n, there is a prime number, is constructive: "Let n be an arbitrary number. Form the number 1*2*...*n + 1. Like every number greater than 1, this number has at least one prime factor. This factor is necessarily a prime numbers larger than n."

In contrast, nonconstructive proofs may contain case distinctions which we cannot decide by an algorithm, like "either set X is infinite, in which case foo, or it is not, in which case bar". Hence such proofs do not contain descriptions of algorithms.

So far so good. Amazingly, there are techniques which can sometimes constructivize given nonconstructive proofs, even though the intermediate steps of the given nonconstructive proofs are simply out of reach of finitary algorithms. In my research, it happened several times that using these techniques, I obtained an algorithm which worked; and for which I had a proof that it worked; but whose workings I was not able to decipher for an extended amount of time. Crazy!

(For references, see notes at rt.quasicoherent.io for a relevant master's course in mathematics/computer science.)