Can programming help one understand constructive mathematics? 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?
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.