In sixties the opinion that mathematics cannot be practically formalized was well established. So the main achievement of de Bruijn, among many others, is the decision that the problem must be reconsider and probably positively solved. And I believe that 1967 will be treated by future historians of mathematics as a turning point.
It is not easy to say precisely what we learnt in the meantime, if we learnt anything at all. I believe that the most important results are:
Still we should me more concerned with the original ideas of de Bruijn, the most important that eventually we have to be able to formalize new mathematical results, published in mathematical newspapers in this century.