[Tainnor]

> because type theory can be verified by a computer

proofs in FOL can be checked by a computer without any need for type theory - just look at metamath.