Hacker News

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

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

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

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

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

The name is amusingly ironic now.

Also, I dislike that they are using Github as the default package registery. But as this langage was created inside Microsoft, it makes senses.

Static linking wonders?

Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.

Lean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.

Imo F* is a much better choice for proof-oriented programming than lean4. The latter is still largely about mathematics while the former has things like https://fstarlang.github.io/lowstar/html/LowStar.html

I don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool.

The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation.

[0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ (Cedar)

C--! I forgot that one. The ILR for the first versions of the Glasgow Haskell Compiler

Indeed! I got to about 20 with A-B-C but it somehow became harder after those. The multitude of C-something is obvious but I didn't realize there's so many A* languages (apl, ada, agda, alice, algol, applescript, apex, ampl, assembly..)

Great post. Thanks!

> scheme: minimalist Lisp dialect used in academia

There are very minimal versions and also huge versions with lot of libraries, batteries and the kitchen sink.

The author is named Alok, so I would expect alokscript to be a self-authored programming language. But I checked the GitHub profile and I don't see anything.

Common Lisp through SBCL fits this for everything but changing GC strategies. I'm not sure why you'd do that, though. SBCL's generational GC is faster in all cases, easy to reason about, and trivial to pause.

In many of these other categories, clisp exceeds requirements. The REPL and Doc situation is so good it's honestly worth it for those alone. People put up with `):'(,@ soup for good reason.

I believe there are tradeoffs which is why this doesn't exist. Isn't the compile speed of Go so good because it's type system is much simpler?

What do you like so much about Kotlin type system, and document / testing of elixir?

> The result monad/option monad and match statements from OCaml/Gleam

Do you mean actual monads or just the specific result/option containers? If you mean a fully-fledged monad abstraction then you need a more sophisticated type system than what Kotlin provides (i.e. higher-kinded types).

performance of Go - why not Fortran? type system of Kotlin - why not Scala/Haskell? Repl like Kotlin, why not Clojure?

"The compile speed of Go" - Delphi starts laughing

- The reach of JavaScript

I believe you can thank Verso for that:

https://github.com/leanprover/verso

It is verso. My understanding is that it's like really fancy javadocs that makes communicating Lean code easier for everyone.

https://github.com/leanprover/verso

You mentioned there are reasons not to type check your program. I would very much like to hear what they are!

Also, I have to point out that of course Ruby has types. And it does type checking. It just does it when the line of code actually runs. (i.e. runtime type errors).

So the discussion here isn't should we check types or not. It's a question of when to do it.

Do you want to know you've made a mistake when you actually make it? Or do you want to find out an unknown amount of time later (e.g. in unfortunate cases, several months later, debugging an issue in prod. Not that I would know anything about that ;)

---

My own thinking on the subject is that it should be configurable.

Rust's level of correctness, for example is probably overkill for a game jam. (As is, arguably, using a low level language in the first place.)

But my thinking here is that correctness should be opt out rather than opt-in. If you have a good reason to make your program wrong by default, then you should be allowed to do that. But it should be a conscious choice! And every source file, at the top of the file, should remind you that you are making that choice: #JAMMODE

And if you intend to actually ship the thing, and charge money for it, in Serious Release Mode the compiler should refuse to build anything that's still in jam mode.

My point here is that some languages make jam mode the only option you have.

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

Who else would add them, besides people who want them? I'm confused about what you're even claiming here. It sounds like you feel that there's a vocal minority of type enthusiasts who everyone else is just humoring by letting them bolt on their type systems.

> do not acknowledge trade-offs when it comes to type systems

Could you elaborate?

Well Ruby kinda brought forth Crystal which while its own Programming Language is kinda Ruby but with Types.

> How about lisp?

I was wondering why lisp (and forth) were omitted from the initial list of languages named in the post.

I guess Scheme is in the list has ok macros.

> > languages without types tend to grow them, like PHP in 7.4 and Python type annotations

...

> Not everyone shares that opinion. See ruby.

All programming languages that have values (i.e. all of them) have types, because you cannot have a concrete value that doesn't have a type. This includes Ruby.

The only difference is whether the language lets you annotate the source code with the expected type of each value.

This is why you observe that all languages trend towards visible typing: The types are already there and it's only a matter of whether the language lets the programmer see it, or lets a linter enforce it, and everyone likes linters.

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

Maybe you misidentified where the type declaration is coming from? It might not be coming from people who want to see types in the source code, it most probably is coming from people who want a decent linter.

In 2026, programming without type-enforcement is like programming using an LLM; it's quicker, but less safe.

Here's a recent talk about how "concrete syntax matters, actually": https://www.youtube.com/watch?v=kQjrcSMYpaA

Highly recommended!

Who said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that this proof will most likely be an implicit argument, that would be a really annoying thing to use.

On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error:

  def x := #[1, 2, 3, 4]
  #check x[7]

These are both pretty reasonable semantics for these functions. `UInt8.ofNat : Nat -> UInt8` might reasonably map the infinite number of `Nat` values to `UInt8` by taking the natural number modulo 256. And it's sensible enough that subtraction with natural numbers should saturate at 0.

These aren't the only reasonable semantics, and Lean will certainly let you define (for instance) a subtraction function on natural numbers that requires that the first argument is greater than or equal to the second argument, and fail at compile time if you don't provide a proof of this. These semantics do have the benefit of being total, and avoiding having to introduce additional proofs or deal with modeling errors with an `Except` type.

Good point, and an important example why static types are ultimately a failure: Encoding the actual invariants in them you care about is a pain in the ass.

No doubt there will be plenty of comments to your comment trying to rationalise this.

There are community-built editor supports. For example,

- Emacs: https://github.com/leanprover-community/lean4-mode

- Neovim: https://github.com/Julian/lean.nvim

I'm using the Emacs lean4-mode and it's pretty good.

It makes complete sense to polish that usecase.

Wow, I read the whole thing without noticing that.

But as someone who came of age in the AIM / ICQ / IRC days, it feels pretty normal. That's just how we wrote. I still fall into it by accident when the context is right and I'm not thinking about it (eg Slack at work). I hope youngsters aren't judging me for it.

I think this is just applying the same informal writing style used in, for example, online chats with friends, to a relatively-informal blog post. I don't think this has anything to do with the Bay Area or its tech industry in particular.

YES, THIS (capitalized on purpose). Folks, please use reasonably correct writing syntax. You CAN do better .. At least think of the AIs consuming your writings.

its not caused by a habit of writing authentically formatted Homestuck rp smut

but surely its correlated

It communicates a certain tone that is sometimes what one is going for. I do it in HN comments sometimes if I'm feeling, like, dry or dismissive.

Is it due to the feature that the author claimed "this blog post is itself Lean code"?

i notoriously ignore using my shift key when im typing informal stuff (comments, chats to coworkers, friends, etc). big ol emails = you'll see me using my shift key.

most of this comes from me noticing how funny sql looks with all the people trying to use caps all over the place as if anyones working in a place without syntax highlighting in 2026. sql is the wild west and everyones sql looks like shit there is no shame. i was told i needed to use caps more early on in sql and i lmfao'd, but i was new to the career and that scarred me. i write lower case sql just to spite others now and if you see something capitalized you know i meant it, but for the most part you have to pay me to use my shift key.

my trauma is now your trauma

It’s to show you’re too cool for grammar rules.

The swearing is another thing I keep seeing more of.