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?
Coding is the purest form of art
1–5 of 5 posts
Re: Coding is the purest form of art
#2I 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.
Re: Coding is the purest form of art
#3If 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.
Re: Coding is the purest form of art
#4‘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
Re: Coding is the purest form of art
#5If 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
Yeah, that's why I mentioned Lean 4, Agda, and Rocq. Homotopy type theory is even better; see it's definition of a circle.