マルティンレーフの構成的型理論は
集合論抜きで数学を構築しようという試みだろう。
しかしながら記述集合論の例では一階述語論理と等価な体系で、
むしろそれを自然言語に合致しない部分について制限を加えたうえで、
ウェブセマンティックスに例えばOWLなんかに転用しようとされている。
これが数学や論理学というならば、建築でのJIS規格での強度計算なんかも
数学や物理学となってしまう。
情報科学は形式化の試みが著しい分野であり、
理論計算機以外での形式化には気を付ける必要があろう。