Post #4405136
2026-08-02 18:11 UTC
Replies (2)
-
@chrisamaphone@hci.social 2026-08-02 18:14
@AmenZwa@mathstodon.xyz for PLFA, note there are two additional authors, Kokke and Siek
-
@AmenZwa@mathstodon.xyz 2026-08-02 18:54
@chrisamaphone@hci.social Yes indeed, Software Foundations is Coq, through and through. But there is an Idris edition as well (by Bailey et al.). As a programmer with a CS background, but one who is not a theoretical CS, I favour Agda/Idris. I recognise that this is a grievous offence to many purists. At present, Agda/Idris adoption appears to lag those of Coq and Lean. These are the reasons why I specifically chose the Agda edition of Software Foundations. https://idris-hackers.github.io/software-foundations/pdf/sf-idris-2018.pdf I have no intention of making a single social media post comprehensive and sealed—because that is impossible. Besides, once a reader reaches the level of delving into Software Foundations, he would have developed his own perspective and taste that would aid him to explore and adopt tools and techniques, as he sees fit. The fact that I am not a CS theoretician, only a CS practitioner, explains how I came up with this list. That is the general, vague answer. But if you are asking the specifics of the "why and how" this list, then the answer is that I read and I share. I have, for the past several decades, been exposing Bird's maxim—programming is a mathematical act—to my colleagues in the IT industry. So, my social media posts and my blog posts tend to focus on industry-friendly, introductory-level CS topics. After more than forty years, I have had only a limited success with this endeavour; the majority of IT practitioners I have worked with are not CS and even those who are CS are not interested in the traditional mathematics-based approaches that I was taught in the early 1980s. Still, I shall persist in this one-man crusade, until I retire, in a few years.🤷♂️