5 ms·
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 com
by mycroftiv 5y ago
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 5y agoCan you mention some downstream effects such that your life was changed?
- gijvikvff 5y agoI think they just mean that they wouldn't necessarily have heard about or got into Agda otherwise.
- guerrilla 5y agoNow read their answer :)
- mycroftiv 5y agoI 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.
- agumonkey 5y agoSad to hear about your disability.. but somehow your path in life is fascinating.