Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

This post refers to the Curry-Howard isomorphism and the Martin-Löf Type Theory.

The post makes the claim of a future 'unification' between the the describing language of math, and the operation based language of computer programming.

My questions are:

  1. Will these ideas lead to a better ability (through languages) to write provably correct code?

  2. Have the full implications of MLTT been discovered on a theoretical level?

  3. Does this post describe anything could couldn't already do in COQ or Agda?

share|cite|improve this question
up vote 9 down vote accepted

I don't think your question is particularly well posed. It mostly asks for opinions. Here are mine:

  1. Yes.
  2. I do not know what you mean, but the answer is probably "there is more MLTT theory to be done, although we do know a lot".
  3. You cannot do all of homotopy type theory in Coq and Agda. This is an active area of research.
share|cite|improve this answer
Ok - how would you have phrased questions relating to the original post? – hawkeye Nov 16 '12 at 5:05
I don't know because I do not understand what the question is asking. The second question is too broad, and the obvious answer is "no". The third question is ok, I suppose. The first question asks us to predict the future. – Andrej Bauer Nov 16 '12 at 5:08

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.