Dijkstra on proof

That a proof is also the carrier of our understanding and that the joy of understanding is the last one we should delegate to machine is hardly stressed, probably because it cannot serve as a basis for funding.