The first interesting connection I’ve been thinking about for a while is from Michael Baxandall’s patterns of intention. In the book he is looking at how we describe works of our, historically and critically. He begins with a non-art artifact, the Forth Bridge. His descriptions and explanations mesh very well with software. Unlike literature, art is non-linear. Where we start with our explanation is a choice in itself. We also face this problem of translation. One way to full describe an image is to list all its pixels. But this is hardly what we mean by description. There is a ton more in this book, really well written and interesting. It leads me to ask the question, what would code criticism look like? There are traditions that take up that name. There is some interesting work there, but they are in the vein of critical studies rather than art/literary criticism. My very basic start of this project was to think about the elements of describing code style. We have them very clearly in art, but to my knowledge, not shared vocabulary for describing code. My elements are very basic. But I think recognizable and hopefully useful. https://jimmyhmiller.github.io/aesthetic-elements

The second influence I’ve been considering is the philosophical literature on Conceptual Engineering. The idea is that concepts in our language are not static, but rather change over time. There are questions about how exactly these change, how much is in our control etc. But what is really interesting, is all of the philosophical literature points to us, software engineers, as the quintessential example conceptual engineering. Yet we never talk about that concept. I think consciously thinking about our work as conceptual engineering might actually shed some light on it. https://jimmyhmiller.github.io/conceptual-engineering

@Konrad Hinsen Definitely agree formalization is a subset of Conceptual Engineering. Also really like your thoughts on domain specific type systems and gradually layering on types. I’ve done a few very basic proofs in idris using the type system. But the proof I actually understood the most was when I used idris without all the fancy types to walk through Godel’s incompleteness theorems. My code will type check and not be a correct proof, but I understood it so much more. And I had a much better time writing it. I often find when I am reading analytic philosophy I wish I had a nice programming tool for exploring the various formal arguments I encounter. https://github.com/jimmyhmiller/PlayGround/blob/master/idrisTests/src/Godel.idr