Per Martin-Löf writes so beautifully.<p>Here’s more: <a href="https://github.com/michaelt/martin-lof" rel="nofollow">https://github.com/michaelt/martin-lof</a><p>Here’s another one - this one is wonderful: <a href="https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-retypeset-1984.pdf" rel="nofollow">https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Bo...</a><p>As far as I understand the theory, then dependently typed languages such as Idris have their roots in his work on intuitionistic type theory: <a href="https://en.wikipedia.org/wiki/Intuitionistic_type_theory" rel="nofollow">https://en.wikipedia.org/wiki/Intuitionistic_type_theory</a><p>Intuitionism in math is beautiful imo: <a href="https://en.wikipedia.org/wiki/Intuitionism" rel="nofollow">https://en.wikipedia.org/wiki/Intuitionism</a>
As a layman I'm curious about the state of constructivist mathematics and intuitionism since the tragic passing of Vladimir Voevodsky in 2017. I recall reading about the Coq proof assistant, homotopy type theory, and univalent foundations with some interest, but I haven't been keeping up with any new developments -- is it still an active field of research?<p>I'm also curious if someone can weigh in on the fact that this paper by Martin-Löf finishes with a proof of the axiom of choice -- isn't that a bit of a controversial axiom? Does all of constructivist mathematics still depend on the axiom of choice to this day?
Very interesting. Amazing how much we owe, without realizing, to the early pioneers and designers of the first computers, who often prognosticated issues we deal with today.<p>I recently have been researching Leslie Lamport's TLA+ project. Definitely in line with the ideas in this paper.
<a href="https://lamport.azurewebsites.net/tla/tla.html" rel="nofollow">https://lamport.azurewebsites.net/tla/tla.html</a>
Thanks, I'll copy this to my tablet so I can carry it around with me.<p>Looking forward to being impressed (hopefully) that it is still relevant today.
Few years ago I joined some metaphysical dots between "construction", "constructivism", "creation" and "creationism" in my head, which is what led me on to explore 100 years of history/theory behind computational trinitarianism, intuitionistic logic, Curry-Howard isomorphism etc.<p>This conceptual understanding of Monist metaphysics was the end of my militant atheism.<p>The expression of knowledge is the creation of knowledge.<p>It pleases me to see that Per Martin-Löf joined the same dots in his paper "A path from logic to metaphysics".