Typeteori er oprindelig udsprunget fra ønsket om at beskrive de langt rigere universer af data man finder i programmer end man finder f.eks. i fysikken. Typeteori opstod således udfra ønsket om at hjælpe programmørerne med at konstruere fejlfri programmer ved først at typebestemme alle data, beregninger og processer -- før programmøren beskrev beregningernes algoritmiske, eller processernes opførselsmæssige forløb. Men typeteori er gået langt videre. Som man kan løse mange opgaver i fysik ved almindelige dimensionsbetragtninger, således kan for eksempel udtryk i intuitionistisk typeteori beskrive beregninger. Man må nok idag konstatere at datalogisk typeteori er en af den teoretiske datalogi's fundamentalt nye bidrag til videnskaben -- og til matematikken?