[loicd]

> The rejection of double-negation elimination is more or less the (rather intuitive) idea that knowing why something must be true doesn't automatically mean you know how it's true.

Exactly. There is also the matter of efficiency: it is easier to know why something must be true than to know how it's true. Constructibility in mathematics usually means proving things the hard way.