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

<ol>
<li>Yes.</li>
<li>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".</li>
<li>You cannot do all of homotopy type theory in Coq and Agda. This is an active area of research.</li>
</ol>

CC BY-SA 3.0
2012-11-16T05:05:09.297Z
Ok - how would you have phrased questions relating to the original post?
hawkeye
CC BY-SA 3.0
2012-11-16T05:08:31.550Z
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
CC BY-SA 3.0
2012-11-16T04:04:34.077Z
2012-11-16T04:04:34.077Z
Andrej Bauer
<p><a href="http://spin.atomicobject.com/2012/11/11/unifying-programming-and-math-the-dependent-type-revolution/">This post</a> refers to the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence">Curry-Howard isomorphism</a> and the <a href="http://en.wikipedia.org/wiki/Martin-L%C3%B6f_type_theory">Martin-Löf Type Theory</a>. </p>

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

<p>My questions are:</p>

<ol>
<li><p>Will these ideas lead to a better ability (through languages) to write provably correct code?</p></li>
<li><p>Have the full implications of MLTT been discovered on a theoretical level?</p></li>
<li><p>Does this post describe anything could couldn't already do in COQ or Agda?</p></li>
</ol>

<lo.logic><pl.programming-languages><type-theory><automated-theorem-proving>
Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?
hawkeye
# Will Martin-Löf Type Theory lead to a greater ability to write provably correct code?

(Asked by: username_0 on 2012-11-15)

[This post](http://spin.atomicobject.com/2012/11/11/unifying-programming-and-math-the-dependent-type-revolution/) refers to the [Curry-Howard isomorphism](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence) and the [Martin-Löf Type Theory](http://en.wikipedia.org/wiki/Martin-L%C3%B6f_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?

**Tags:** lo.logic, pl.programming-languages, type-theory, automated-theorem-proving


---

## 1 answers

### Answer by username_1 on 2012-11-16. Score: 10 | Accepted answer

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.

> **Comments:**
> **username_0**: Ok - how would you have phrased questions relating to the original post?  
> **username_1**: 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.  

---

