9
$\begingroup$

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?

|cite|improve this question
$\endgroup$
10
$\begingroup$

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.
|cite|improve this answer
$\endgroup$
  • $\begingroup$ Ok - how would you have phrased questions relating to the original post? $\endgroup$ – hawkeye Nov 16 '12 at 5:05
  • 3
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Nov 16 '12 at 5:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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