Coding is the purest form of art

1 points by learningstud 168 days ago | 4 comments

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?

tromp 168 days ago |

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

learningstud 168 days ago | |

Yeah, that's why I mentioned Lean 4, Agda, and Rocq. Homotopy type theory is even better; see it's definition of a circle.

nacozarina 168 days ago |

‘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

Trasmatta 168 days ago |

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.