4
$\begingroup$

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?

$\endgroup$
8
$\begingroup$

Agda 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.

$\endgroup$
2
$\begingroup$

Maybe take a look at the textbook Software Foundations, which uses the proof assistant Coq. 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, 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.

$\endgroup$

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.