<p><a href="http://wiki.portal.chalmers.se/agda/pmwiki.php">Agda</a> is a dependently typed programming language and/or proof assistant for Martin-Löf type theory. Programming in Agda feels very much like programming in Haskell. For example, inductive proofs are written as recursive functions with multiple equations that pattern match on the function arguments. So programming and/or proving in Agda is a good way to learn about constructive mathematics coming from a (functional) programming background.</p>

CC BY-SA 3.0
2014-09-22T09:00:40.540Z
2014-09-22T09:00:40.540Z
Toxaris
<p>Maybe take a look at the textbook <a href="http://www.cis.upenn.edu/~bcpierce/sf/current/index.html" rel="nofollow">Software Foundations</a>, which uses the proof assistant <a href="http://coq.inria.fr/" rel="nofollow">Coq</a>. I don't think the focus is really on "learning constructive math", but it does develop the programming tools. On the other end of the spectrum is the <a href="http://homotopytypetheory.org/book/" rel="nofollow">Homotopy Type Theory Book</a>, which is very theoretical about constructive math, but doesn't include programming per se (I think). I don't know if there's a book in the middle, that focuses on proof assistants for constructive math.</p>

CC BY-SA 3.0
2014-09-23T14:39:13.580Z
2014-09-23T14:39:13.580Z
usul
<p>I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the subject. As a student in computer science, I have a background in programming, and I was wondering if programming in a language like Haskell would help in this endeavor? If not Haskell, then which programming language is best suited for learning constructive math?</p>

<functional-programming><haskell><constructive-mathematics>
Can programming help one understand constructive mathematics?
Ali
# Can programming help one understand constructive mathematics?

(Asked by: username_0 on 2014-09-22)

I have read about the principles of constructive mathematics, for example, the principle of excluded middle is not allowed, and now I want to do some exercises to increase my understanding of the subject. As a student in computer science, I have a background in programming, and I was wondering if programming in a language like Haskell would help in this endeavor? If not Haskell, then which programming language is best suited for learning constructive math?

**Tags:** functional-programming, haskell, constructive-mathematics

---

## 2 answers

### Answer by username_1 on 2014-09-22. Score: 8

[Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php) is a dependently typed programming language and/or proof assistant for Martin-Löf type theory. Programming in Agda feels very much like programming in Haskell. For example, inductive proofs are written as recursive functions with multiple equations that pattern match on the function arguments. So programming and/or proving in Agda is a good way to learn about constructive mathematics coming from a (functional) programming background.


---

### Answer by username_2 on 2014-09-23. Score: 2

Maybe take a look at the textbook [Software Foundations](http://www.cis.upenn.edu/~bcpierce/sf/current/index.html), which uses the proof assistant [Coq](http://coq.inria.fr/). I don't think the focus is really on "learning constructive math", but it does develop the programming tools. On the other end of the spectrum is the [Homotopy Type Theory Book](http://homotopytypetheory.org/book/), which is very theoretical about constructive math, but doesn't include programming per se (I think). I don't know if there's a book in the middle, that focuses on proof assistants for constructive math.


---

