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.
Well, okay Shriram said the term "homoiconicity" is fuzzy, but the underlying thing (the language of data and the language of programs being the same representation) is real and worth taking seriously. Citing him to wave away the whole concept is pretty wild misuse of the citation. They are refining the claim, not negating it.
> doesn't gain anything semantically
Syntactic properties create semantic affordances. The reason "code as data" matters isn't that the parentheses look a certain way - it's that the AST is a first-class citizen of the runtime data model. Those are semantic capabilities - they determine what programs can express and compute, especially at the meta level. The syntactic uniformity is the mechanism; the ability to write programs that construct and transform other programs, using the same tools as everything else, is the payoff.
Homoiconicity doesn't make Lisp programs mean something different, but it gives you a more uniform and powerful meta-programming model.
I don't disagree with this. Benjamin Pierce defines type-checking in the opening pages of Types and Programming Languages as an operation over syntax, for example.
My point was that the parent comment just kind of threw out "homiconicity" when somebody talked about writing properties about a language in that language, and those are entirely separate things. I was addressing a conflation of terms. The property that people generally refer to as "homoiconicity" is useful for things like writing macros, but it does not directly grant you access to any kind of property-checking capabilitiy. I mean, Rust's macro system is far from homoiconic (it's just an AST), but it gives you semantic capabilities. You know?
it's still far easier to write a metainterpreter to play around with language semantics if you have homoiconic syntax. consider the feasibility of altering the search strategy in prolog compared to changing something about c# linq semantics.
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).
The primary culture around Lean is mathematicians looking to prove mathematics. AFAICT Lean is just about the right power for that.
Agda, OTOH, is IMO the dependently typed language for type theorists, and does weird things, but "unproductive" is applicable only for a somewhat narrow view of productivity.
I don't consider there to be a dependently typed language for writing programs that you just want to run, but I would be delighted to be corrected on that viewpoint!
Yep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.
Since you've clearly looked at this a bit... would you give a sentence or two comparing Indris, F*, and the other lesser known players in this space (languages for both writing and formally verifying programs)? I find it a wide space to explore, and while ecosystem maturity seems like a huge deciding factor right now, I assume there's real and meaningful differences between the languages as well.
Idris is rather unique in that the development flow involves writing out your program as a trellis with "holes", and you work through your codebase interactively filling those holes. It feels like Haskell with an even more powerful type system and a companion expert system to alleviate the burden that the type-system's power entails. You're still basically always in program-land, mentally.
F* (and most other dependently-typed languages, or adjacent ones like Liquid Haskell) has a whole external SMT solver layer that lives outside of the language. Think like if SML modules were even less unified with the core language, and also most of your time was spent in that layer. They're really not fun to try and make complex software with, just because the context-switching required at scale is borderline inhuman.
Lean has a unified proof-system in the language like Idris, but it has much the same grain as the languages with external SMT solvers. You're spending most of your mental time in proofsland, thinking primarily about how to prove what you want to do. That's because with how Lean as a language is set up, you're basically centering all your reasoning around the goal. If there's a problem, you're adjusting the structure of your reasoning, changing your proof strategy, or identifying missing lemmas, etc.
You can kind of think of it as though Idris is "inside out" compared to most of the other dependently typed languages.
It's been a little bit since I looked at Idris, so I'll take a closer look now. The QTT behind it struck me as interesting but I didn't play around with it much. Thanks for the tip!
Practical Lispers would like to have a word - I've been witnessing extreme productivity on some teams.
Modern Lisp dialects (Clojure and likes) largely broke library fragmentation and the "not invented here" tendency that were causing real tensions in Common Lisp.
You realize that "The Lisp Curse" isn't some paper, survey or objective reflection? It's just someone's essay back from 2011 - an opinion.
You can take it word-by-word and apply to say Javascript, and it would largely feel true - JS arguably has the worst fragmentation of any ecosystem; dozens of competing frameworks, build tools, bundlers, test runners; new frameworks constantly replacing old ones; "Javascript fatigue" is a real thing, etc., but nobody talks about "Curse of Javascript"
I learned Lisp (once) and that opened up path to Clojure, Clojurescript, then Fennel, Janet and Clojure-Dart, libpython-clj, there's Jank that is about to break loose. And something opposite to fragmentation happened to me - all these incompatible runtimes became unified and controllable from the same substrate - I no longer feel like I'm having to switch between languages - the syntax and thinking stays stable. The runtime is just a deployment target.
The curse essay says: "Lisp empowers fragmentation". Actual experience says: "Lisp provides unity across fragmentation that already existed"
Then again sometimes things don’t need to have productivity as a goal do they? Scale and context applies, could be seen as art even, an expression of someone’s psyche and their world model
Unfortunately Lean’s distribution went from somewhat about 15 MiB in times of Lean 3 to more than 2,5 GiB when unpacked nowadays for no good reason. This is too much. Even v4.0.0-m1 was a 90 MB archive. Looks like that Lean’s authors do not care about this anymore.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
i love lean4, best in class functional programming language. but i think its "perfectability" is kinda hamstrung by baking non-constructive axioms into the standard library. the kernel has to treat these as opaque constants that cannot be reduced.
i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
Are they actual project running some business in the wild? I only played with coq in university, while I saw F# being employed in insurance companies. I only heard about lean through HN posts.
> languages without types tend to grow them, like PHP in 7.4 and Python type annotations
Well ... that is a trend that is driven largely by people who love types.
Not everyone shares that opinion. See ruby.
It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems.
So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types. I saw this happen "live" in ruby; I am certain this happened in python too.
> inevitably, people want to push types. even Go. C++ templates are the ultimate example. if it can be computed at compile time, at some point someone wants to, like Rust's ongoing constification.
And many people hate C++ templates. But comparing that language to e. g. ruby is already a losing argument. Languages are different. So are the trade-offs.
> dependent types can get you there. hence perfectable.
So the whole point about claiming a language is "perfectable", means to have types? I don't agree with that definition at all.
> most languages have no facility for this,
How about lisp?
> this lets you design APIs in layers and hide them behind syntax.
The language already failed hard syntax-wise. This is a problem I see in many languages - 99% of the language designers don't think syntax is important. Syntax is not the most important thing in the world, but to neglect it also shows a lack of understanding why syntax ALSO matters. But you can not talk about that really - I am 100% certain alok would disagree. How many people use a language also matters a LOT - you get a lot more momentum when there are tons of people using a language, as opposed to the global 3 or 4 using "lean".
For anyone as curious as me, here's short description for each language in the list (excluding most common ones):
cyclone: safe C dialect preventing memory errors
zig: modern systems language with explicit control over memory
odin: another modern systems language
nim: Python-like syntax, memory safe, compiles to C/C++/JS
visual basic: event-driven language for Windows GUI apps
actionscript: language for Adobe Flash applications
php: server-side scripting for web development
typescript: JavaScript with static types
elm: functional language that compiles to JS, no runtime errors
purescript: Haskell-like language compiling to JS
haskell: purely functional, lazy language with strong types
agda: dependently typed functional language for theorem proving
idris: dependently typed language for type-driven development
coq: proof assistant based on Calculus of Inductive Constructions
isabelle: interactive theorem prover
clean: purely functional language with uniqueness typing
unison: content-addressed functional language with hashes instead of names
scheme: minimalist Lisp dialect used in academia
racket: a Scheme/Lisp dialect for language-oriented programming
prolog: logic programming with backtracking
ASP: Answer Set Programming for combinatorial search
clingo: ASP solver for logic-based reasoning
zsh: extended Bourne shell with advanced scripting
tcsh: enhanced C shell with command-line editing
awk: pattern-directed text processing language
sed: stream editor for text transformation
hack: PHP-derived language with gradual typing
verilog: hardware description language for digital circuits
whitespace: esoteric language using only spaces, tabs, newlines
intercal: esoteric language designed to be confusing
alokscript: can't find anything =(
- The compile speed of Go
- The performance of Go
- The single binary compilation of Go
- The type system of Kotlin
- The ecosystem of JVM (packages for anything I could dream of)
- The document sytem/tests of Elixir
- The ability to go "unsafe" and opt for ARC instead of GC
- The result monad/option monad and match statements from OCaml/Gleam
- A REPL like Kotlin or even better, OCaml
- A GREAT LSP for NeoVim
- A package/module system that minimizes transient dependencies
- No reliance on a VM like BEAM or JVM
I still dream about this "one size fits all" language.
> For Eliza Zhang, who bet I couldn’t write a web app in C in one week using only the standard library. She was right. I didn’t know what any of those words meant. But I said the fuck I can’t, and that’s how I got into coding.
interesting the ones they chose to name; I would have probably started with 6502/68000/68020/z80 assembly, fortran, cobol, basic, c, ada, simula 67, sh, zsh, bash, napier 88, tcl, perl, rexx, before hitting the next generation of python, c++, etc.
fwiw, I think a similar tik-tac-toe evaluator could be made in rust declarative macros, no proc macros needed. I’ll see if I can smuggle some experimentation time today to make an example.
The thing I found really surprising about Lean is that although it is really focused on proving stuff, it has some surprisingly enormous footguns. What do you think the result of these are?
The first should be a compile time error right, because UInt8.ofNat is going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give a Nat unless the first argument is definitely more than the second.
What is up with so many people doing weird capitalization now? Is this some Bay-tech flex? Alok writes their own name, and other names, with leading caps, but not the first word in sentences? It makes it so uncomfortable to read.
143 comments
Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.
[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...
> doesn't gain anything semantically
Syntactic properties create semantic affordances. The reason "code as data" matters isn't that the parentheses look a certain way - it's that the AST is a first-class citizen of the runtime data model. Those are semantic capabilities - they determine what programs can express and compute, especially at the meta level. The syntactic uniformity is the mechanism; the ability to write programs that construct and transform other programs, using the same tools as everything else, is the payoff.
Homoiconicity doesn't make Lisp programs mean something different, but it gives you a more uniform and powerful meta-programming model.
> Citing him to wave away the whole concept is pretty wild misuse of the citation.
Good thing I didn't do that?
> Syntactic properties create semantic affordances.
I don't disagree with this. Benjamin Pierce defines type-checking in the opening pages of Types and Programming Languages as an operation over syntax, for example.
My point was that the parent comment just kind of threw out "homiconicity" when somebody talked about writing properties about a language in that language, and those are entirely separate things. I was addressing a conflation of terms. The property that people generally refer to as "homoiconicity" is useful for things like writing macros, but it does not directly grant you access to any kind of property-checking capabilitiy. I mean, Rust's macro system is far from homoiconic (it's just an AST), but it gives you semantic capabilities. You know?
Agda, OTOH, is IMO the dependently typed language for type theorists, and does weird things, but "unproductive" is applicable only for a somewhat narrow view of productivity.
I don't consider there to be a dependently typed language for writing programs that you just want to run, but I would be delighted to be corrected on that viewpoint!
F* (and most other dependently-typed languages, or adjacent ones like Liquid Haskell) has a whole external SMT solver layer that lives outside of the language. Think like if SML modules were even less unified with the core language, and also most of your time was spent in that layer. They're really not fun to try and make complex software with, just because the context-switching required at scale is borderline inhuman.
Lean has a unified proof-system in the language like Idris, but it has much the same grain as the languages with external SMT solvers. You're spending most of your mental time in proofsland, thinking primarily about how to prove what you want to do. That's because with how Lean as a language is set up, you're basically centering all your reasoning around the goal. If there's a problem, you're adjusting the structure of your reasoning, changing your proof strategy, or identifying missing lemmas, etc.
You can kind of think of it as though Idris is "inside out" compared to most of the other dependently typed languages.
> you end up with an unproductive culture
Practical Lispers would like to have a word - I've been witnessing extreme productivity on some teams.
Modern Lisp dialects (Clojure and likes) largely broke library fragmentation and the "not invented here" tendency that were causing real tensions in Common Lisp.
You realize that "The Lisp Curse" isn't some paper, survey or objective reflection? It's just someone's essay back from 2011 - an opinion.
You can take it word-by-word and apply to say Javascript, and it would largely feel true - JS arguably has the worst fragmentation of any ecosystem; dozens of competing frameworks, build tools, bundlers, test runners; new frameworks constantly replacing old ones; "Javascript fatigue" is a real thing, etc., but nobody talks about "Curse of Javascript"
I learned Lisp (once) and that opened up path to Clojure, Clojurescript, then Fennel, Janet and Clojure-Dart, libpython-clj, there's Jank that is about to break loose. And something opposite to fragmentation happened to me - all these incompatible runtimes became unified and controllable from the same substrate - I no longer feel like I'm having to switch between languages - the syntax and thinking stays stable. The runtime is just a deployment target.
The curse essay says: "Lisp empowers fragmentation". Actual experience says: "Lisp provides unity across fragmentation that already existed"
i talked about the lisp curse in this old paper. it's rough but explicitly mentions it
> 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.
Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. This is very sad.
Personally, I stopped using Lean after the last update broke unification in a strange way again.
i tend to stick with agda for doing mathy programming. i kinda want lean4 to replace haskell at some point in the future as the workhorse production typed fp language.
Fun challenge. Unlike the author, I have nothing really to add.
I just wanted to say that "I did NOT write it with ..."
https://github.com/dharmatech/symbolism.lean
Lean is astonishingly expressive.
> the easiest way to do anything is properly.
Oh, what a beautiful world it would be if this were the case!
> at a party, Sydney Von Arx asked if i could name 40 programming languages.
An attempt (without looking)
JavaScript QBasic PHP Haskell C C++ Ada Algol Racket Scheme Clojure Common-Lisp GOOL Fortran Awk Postscript Forth C# F# Lua Java D Odin Rust Zig Julia Python Nim MATLAB Bash Brainfuck Arnold-C Intercal Gleam Unison Ruby Crystal Erlang Go TCL
Phew!
"There are only two kinds of languages: the ones people complain about and the ones nobody uses". - Bjarne Stroustrup
> languages without types tend to grow them, like PHP in 7.4 and Python type annotations
Well ... that is a trend that is driven largely by people who love types.
Not everyone shares that opinion. See ruby.
It is very hard to try to argue with people who love types. They will always focus on "types are great, every language must have them". They, in general, do not acknowledge trade-offs when it comes to type systems.
So the claim "tend to grow them" ... it is not completely wrong, but it also does not fully capture an independent want to add them. It comes ALWAYS from people who WANT types. I saw this happen "live" in ruby; I am certain this happened in python too.
> inevitably, people want to push types. even Go. C++ templates are the ultimate example. if it can be computed at compile time, at some point someone wants to, like Rust's ongoing constification.
And many people hate C++ templates. But comparing that language to e. g. ruby is already a losing argument. Languages are different. So are the trade-offs.
> dependent types can get you there. hence perfectable.
So the whole point about claiming a language is "perfectable", means to have types? I don't agree with that definition at all.
> most languages have no facility for this,
How about lisp?
> this lets you design APIs in layers and hide them behind syntax.
The language already failed hard syntax-wise. This is a problem I see in many languages - 99% of the language designers don't think syntax is important. Syntax is not the most important thing in the world, but to neglect it also shows a lack of understanding why syntax ALSO matters. But you can not talk about that really - I am 100% certain alok would disagree. How many people use a language also matters a LOT - you get a lot more momentum when there are tons of people using a language, as opposed to the global 3 or 4 using "lean".
I've been wanting to adopt Lean for a project but wasn't sure about the speed. Nice to hear that it should be good on that front.
> For Eliza Zhang, who bet I couldn’t write a web app in C in one week using only the standard library. She was right. I didn’t know what any of those words meant. But I said the fuck I can’t, and that’s how I got into coding.
UInt8.ofNatis going to require that its argument is 0-255. And the second should be a compile time error because subtraction should not give aNatunless the first argument is definitely more than the second.Nope! Both give 0.
>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,
Lol