Coding is the purest form of art
As I was watching a YouTube video on Michelangelo's "Pieta", I was reminded of Milton's "Paradise Lost". Though the latter takes a lot more patience to appreciate. Then, I thought of Knuth's "The Art of Computer Programming"; only then did I realize how aptly titled was the book. It struck me that coding could possibly be the purest form of art. It is art constructed of pure thought if only we have a capable enough language to write beautiful prose in it. Lean 4 and Agda come to mind which are more term-based than tactic-based as in Rocq (formally, Coq). Not only could Knuth's book be made an epic in homotopy type theory, it can be the most practical piece of art at the same time. What do you think?
4 comments
If coding is the purest form of art, then lambda calculus may be the purest form of code. Its graphical representation [1] also looks somewhat artistic.
[1] https://tromp.github.io/cl/diagrams.html
[1] https://tromp.github.io/cl/diagrams.html
Yeah, that's why I mentioned Lean 4, Agda, and Rocq. Homotopy type theory is even better; see it's definition of a circle.
‘programming is the art of creating machines simply by describing them.’
it’s the closest thing to ‘spell-casting magic’ I’ll ever know, it finds ways to stay fresh
it’s the closest thing to ‘spell-casting magic’ I’ll ever know, it finds ways to stay fresh
I do think it can be an art form, and definitely a craft. That's one reason I'm so disheartened by the push to have AI slop replace all our coding efforts.