The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

2016-05-31 18:10 GMT+02:00 Kenneth Adam Miller <kennethadammiller AT gmail.com>:

When I asked what I did about type theory, I was almost certain that it was wrong. It seems clear to me now that whereas type theory is a meta-mathematical system for, at lower levels, ensuring that stuck states do not occur, and at higher levels expressing proofs through the curry howard isomorphism.

Don't think about lower or higher levels: all these are just plain math proofs. That's all. Type theory is exactly like Set theory: a universal language for maths concepts and proofs. Applying to semantics happens to be a frequent pattern but this is incidental.

P.