[mycroftiv]

I found this post and the code and math so fascinating it changed my life when I found it three years ago. I did not previously understand the capability of computers to work with the abstract logic of infinite sets in a meaningful way and it led me into the world of formalization of mathematics in the dependently typed programming language Agda, which is one of the current activities of the mathematician (Martin Escardo) who wrote this guest blog post.

[bckr]

Can you mention some downstream effects such that your life was changed?

[mycroftiv]

I made the study of mathematical logic and the connections between set theory and type theory and formalization in Agda my full-time focus. Increasing physical disability ended my career as a performing musician a few years ago and I had a life-long interest in philosophical topics connected with infinity. In the past two years I've written over 100,000 lines of Agda code as a product of my learning and research. I'd like to figure out a type-theoretical translation of the set-theoretic large cardinal axioms at the level of measurable and beyond.

[gijvikvff]

I think they just mean that they wouldn't necessarily have heard about or got into Agda otherwise.