De Bruijn begon in 1967 een nieuw project, "Automath", dat een van de meest originele projecten blijft in de geschiedenis van de verificatie van wiskunde. Om zo'n systeem te kunnen bouwen, moesten De Bruijn en zijn groep nieuwe fundamenten leggen in de formalisering van typetheorie en herschrijfsystemen. Die nieuwe fundamenten blijven invloedrijk tot op de dag van vandaag. In deze voordracht geef ik een kort overzicht van een paar van die uitgangspunten. Ik zal proberen uit te leggen hoe die ideeen van De Bruijn en zijn groep zijn gebruikt, niet alleen in de verificatie van wiskunde, maar ook in programmeertalen.