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?
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.
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.
