logoalt Hacker News

kleiba2today at 7:51 AM5 repliesview on HN

> because it's perfectable. it's not perfect, but it is perfectable. you can write down properties about Lean, in Lean.

Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.


Replies

DonaldPShimodatoday at 6:41 PM

Hm. Homoiconicity is not a well-defined term (see, for example, Shriram Krishnamurthi's thoughts [0][1]), but even skimming over that fact, it is a syntactic property, while the quoted line is about semantics. Switching your language to Lisp (or one of its descendents) doesn't gain you anything semantically.

[0] Shriram is an original member of the Racket project, so he's been working in the Lisp-like domain for at least 30 years and, specifically, he works in an offshoot of Lisp that is particularly concerned with questions of syntax. I think this establishes him as a reasonable citation for this topic.

[1] https://parentheticallyspeaking.org/articles/bicameral-not-h...

show 1 reply
harperleetoday at 12:55 PM

The question then is how they plan to avoid The Lisp Curse (in my words, language giving you too much power makes you do weird things, and you attract people to like to use things a tad too powerful / generic, and you end up with an unproductive culture).

show 3 replies
mghackerladytoday at 1:08 PM

I can't view the site (Org blocks github for reasons) but I suspect this would be a lot like forth if forth weren't so stack focused

show 1 reply
iLemmingtoday at 3:28 PM

> Homoiconicity anyone?

I'm just leaving this here for anyone interested, seems relevant: https://github.com/replikativ/ansatz

Ansatz is a verified programming library for Clojure built on the Calculus of Inductive Constructions (CIC) — the same type theory that powers Lean 4.

patrickmaytoday at 5:11 PM

I came here to comment "We already have Lisp."