[HN Gopher] A perfectable programming language
___________________________________________________________________
A perfectable programming language
Author : yuppiemephisto
Score : 200 points
Date : 2026-04-12 21:11 UTC (1 days ago)
(HTM) web link (alok.github.io)
(TXT) w3m dump (alok.github.io)
| spankalee wrote:
| 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.
| JuniperMesos wrote:
| 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.
| losvedir wrote:
| 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.
| noosphr wrote:
| we wrote like that because each message was a single sentence
|
| if you wanted more than one sentence you sent one then wrote
| the other
|
| it's painful to read longform
|
| the victorians didn't give up on punctuation and regular
| english just because they had the telegraph
| giancarlostoro wrote:
| The swearing is another thing I keep seeing more of.
| trueno wrote:
| 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
| binary132 wrote:
| Only you can stop generational SQL abuse. Capitalize
| keywords, indent grouped syntax, and use prefix commas on
| newlines. Write readable code, for God's sake, you filthy
| heathens.
| QuadmasterXLII wrote:
| its not caused by a habit of writing authentically formatted
| Homestuck rp smut
|
| but surely its correlated
| bobanrocky wrote:
| 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.
| Joel_Mckay wrote:
| I ReSpEcTfUlLy DiSaGrEe FrIeNd -- PeOpLe LoVe SlOp. =3
| jason1cho wrote:
| Is it due to the feature that the author claimed "this blog
| post is itself Lean code"?
| GeoPolAlt wrote:
| It's to show you're too cool for grammar rules.
| ajkjk wrote:
| 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.
| ilsubyeega wrote:
| i like this website, it shows documentation when hovering the
| code while i see similar stuffs really rare in web blog areas
| md224 wrote:
| I believe you can thank Verso for that:
|
| https://github.com/leanprover/verso
| zem wrote:
| this is the log post that put lean on my radar, though I haven't
| played with it yet: https://kirancodes.me/posts/log-ocaml-to-
| lean.html
| snthpy wrote:
| Great post. Thanks!
| travisgriggs wrote:
| Fortran, Basic, APL, Beta, Odin, Self, C, C++, Objective-C, C#,
| C--, D, Scheme, Clojure, F-Script, Eiffel, COBOL, Ocaml, Haskell,
| Snobol, Crystal, Forth, Python, Lisp, Brainfuck, Java, Oak,
| Javascript, TypeScript, Wasm, Logo, Elang, Elixir, Gleam, Elm,
| Zig, m4, Tcl, Simula, Smalltalk
|
| Fun challenge. Unlike the author, I have nothing really to add.
|
| I just wanted to say that "I did NOT write it with ..."
| riffraff wrote:
| 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..)
| cestith wrote:
| Then there's the actual language ABC. It's in the Basic
| family and has whitespace indentation for structuring flow.
| It directly influenced Python.
|
| You could start your list alphabetically with A, A+, and A++.
| A is derived from APL. A+ is a newer take on A. A++ is
| unrelated. https://a-plus-plus-
| devs.github.io/aplusplus/guide/getting-s...
| jbreckmckye wrote:
| C--! I forgot that one. The ILR for the first versions of the
| Glasgow Haskell Compiler
| solomonb wrote:
| 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.
| landl0rd wrote:
| 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
| eggy wrote:
| Yes, a strong argument, and staying in a line of PLs: F# for
| high-level, and F* <-> Low* for theorem proving and low-level
| coding. I am evaluating F _/ Low_ for verified code on Cortex
| M processor that I am currently trying to write SPARK2014.
| The Cortex A processor is running seL4 for less safety-
| critical tasks. I did look at Lean4 as a scratch for my
| Idris2 itch use cases.
| whacked_new wrote:
| wait, I'm intrigued, it says the blog itself is lean code. How?
| It's rendered, like pollen?
| ajs1998 wrote:
| 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
| heliumtera wrote:
| >The recommended way to install Lean is through VS Code and the
| Lean 4 VS Code extension,
|
| Lol
| adamnemecek wrote:
| It makes complete sense to polish that usecase.
| jinwoo68 wrote:
| 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.
| unexpectedtrap wrote:
| 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.
| c0balt wrote:
| Lean is far off the most bloated one. Isabelle most likely
| takes that spot, the main archive includes a whole vscodium
| among other things.
| senko wrote:
| >> Lean 3 was the least bloated theorem prover _among Lean,
| Coq and Agda, and Lean 4 is the most bloated among this Big
| Three._
|
| > Lean is far off the most bloated one. Isabelle most likely
| takes that spot.
|
| _Among these three_ is the operative phrase here.
|
| I hate to be pedantic, but we _are_ talking about theorem
| provers here :)
| c0balt wrote:
| That is a fair point, thank you for the correction there
| pjmlp wrote:
| Static linking wonders?
|
| Originally Lean was coded in C++, and dynamically linked
| executable, if I remeber correctly.
| unexpectedtrap wrote:
| No, it's still linked dynamically and its kernel is still in
| C++ (see
| https://github.com/leanprover/lean4/tree/master/src/kernel,
| this part of a codebase has hardly changed since Lean 3).
| Almost all the space in the package (more than 2.5 GiB) is
| taken up by .olean/.ilean/.ir files, approximately 1 GiB of
| which is generated from the code of Lean's frontend itself
| (i.e., parser, elaborator, core tactics, and so on) and the
| other 1 GiB from a standard library. As you might guess,
| these files are IR and essentially a compiled Lean's
| environment (something like a Lisp image), so that Lean can
| load them straight up without recompiling and rechecking
| everything.
|
| There were some proposals like compressing all the .olean
| files, but (as far as I know) none of them were implemented.
| Well, even if some proposals were implemented, their
| contribution was effectively negated anyway.
| pjmlp wrote:
| Thanks for the overview.
| ebonnafoux wrote:
| Also, I dislike that they are using Github as the default
| package registery. But as this langage was created inside
| Microsoft, it makes senses.
| jandrese wrote:
| The name is amusingly ironic now.
| xarope wrote:
| 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.
| psychoslave wrote:
| 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.
| c0balt wrote:
| 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)
| dharmatech wrote:
| I've been messing around with a computer algebra simplifier in
| Lean:
|
| https://github.com/dharmatech/symbolism.lean
|
| Lean is astonishingly expressive.
| snthpy wrote:
| Very nice!
|
| 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.
| shevy-java wrote:
| > 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".
| ChadNauseam wrote:
| > 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.
| mastermage wrote:
| Well Ruby kinda brought forth Crystal which while its own
| Programming Language is kinda Ruby but with Types.
| andersmurphy wrote:
| > 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.
| rootnod3 wrote:
| I get adding Scheme, but omitting CL seems like a big
| oversight
| vouwfietsman wrote:
| > do not acknowledge trade-offs when it comes to type systems
|
| Could you elaborate?
| patrickmay wrote:
| Here's a good summary of the limited evidence for the
| benefits of strong type systems:
| https://danluu.com/empirical-pl/
| lelanthran wrote:
| > > 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.
| SAI_Peregrinus wrote:
| Some languages have only a single type, e.g. BrainFuck only
| has "byte". Shells tend to only have "string" as a
| fundamental type, and some helpers to do things like split
| strings on a separator & iterate over the elements or to
| treat strings as numbers to do arithmetic. Such single-type
| languages tend to be esoteric and/or difficult to program in,
| since every sort of data manipulation not supported by that
| type has to be done at runtime, by the programmer.
| lelanthran wrote:
| > Such single-type languages tend to be esoteric and/or
| difficult to program in, since every sort of data
| manipulation not supported by that type has to be done at
| runtime, by the programmer.
|
| It depends; I recall programming in Tcl in the late 90s,
| and that has only the string and the list as datatypes, but
| it felt _very_ powerful, like Lisp but without the easy
| syntax.
| jerf wrote:
| I also add the observation that while the dynamic typing
| languages are all growing in the direction of the statically-
| typed languages, no statically-typed language (that I know
| of) is adding a lot of dynamically-typed features. If
| anything the static languages trend towards _more_ static
| typing. Which doesn 't mean the optimum is necessarily "100%
| in the direction of static typing", the costs of more static
| typing do eventually overwhelm the benefits by almost any
| standard, but the trend is universal and fairly clear.
|
| I kind of think there's room for a new dynamically-typed
| language that is designed around being fast to execute and
| doesn't cost such a huge performance multiple right off the
| top, and starts from day 1 to be multi-thread capable, but on
| the whole the trend is clearly in the direction of static
| typing.
| lelanthran wrote:
| > I kind of think there's room for a new dynamically-typed
| language that is designed around being fast to execute and
| doesn't cost such a huge performance multiple right off the
| top, and starts from day 1 to be multi-thread capable, but
| on the whole the trend is clearly in the direction of
| static typing.
|
| Other than the "new" qualifier, Lisp supports all of that -
| SBCL compiles to native code, ecl/gcl compile to C (IIRC),
| etc.
| andai wrote:
| 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.
| ModernMech wrote:
| Here's a recent talk about how "concrete syntax matters,
| actually": https://www.youtube.com/watch?v=kQjrcSMYpaA
|
| Highly recommended!
| danieltanfh95 wrote:
| clojure exists as an example of people trying types and then
| realising it's cruft and not needed.
| IshKebab wrote:
| 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?
| #eval (UInt8.ofNat 256 : UInt8) #eval (4 - 5 : Nat)
|
| 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.
|
| Nope! Both give 0.
| unexpectedtrap wrote:
| 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]
|
| Kevin Buzzard even wrote a blog post about a similar question
| about division by zero:
| https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
| IshKebab wrote:
| > this is definitely not a bad one
|
| It definitely _is_ a bad convention because it 's highly
| surprising. That's what makes it a footgun.
|
| > that would be a really annoying thing to use
|
| Sure. So maybe provide "unchecked" versions for when people
| don't want to bother.
|
| We've known this about interface design for literally
| decades. The default must be safe and unsurprising. You need
| to opt into unsafety.
| unexpectedtrap wrote:
| >It definitely is a bad convention because it's highly
| surprising.
|
| You know that `Nat` represents non-negative numbers, and
| you see that `1 - 2` does not produce a compile error. What
| value do you expect then? What's so surprising about
| choosing zero as a default value here? Do you expect it to
| panic or what?
| IshKebab wrote:
| I would expect it to require a proof that 1 - 2 is non-
| negative. That's kind of the raison d'etre of Lean isn't
| it?
|
| The reason they _don 't_ do that is because Lean treats
| proofs as manually generated explicit objects, unlike
| other languages like Dafny (IIRC) where they are
| implicit. Requiring explicit proofs for every subtraction
| was presumably seen as too onerous.
|
| Which is fine... BUT they then should have said "so we're
| going to define a more convenient operator which is LIKE
| subtraction but isn't actually standard subtraction, and
| therefore _we won 't use the standard subtraction
| notation for it_".
|
| If they had used something like 1 -_ 2 then that would be
| _much_ less surprising because you 'd think "oh right,
| it's the special saturating subtraction".
|
| Similarly for Uint8.ofNat it should have been
| Uint8.ofNatWrapping or similar.
|
| This shouldn't be news.
| unexpectedtrap wrote:
| >I would expect it to require a proof that 1 - 2 is non-
| negative. That's kind of the raison d'etre of Lean isn't
| it?
|
| The reason is to be able to write mathematical proofs,
| including proofs about your code, but not to attach
| proofs to every single function. This definition of
| subtraction does not prevent you from reasoning about it
| and requiring `a >= b` in the proofs/code for which this
| is really important.
|
| >Requiring explicit proofs for every subtraction was
| presumably seen as too onerous.
|
| Lean can deduce proofs implicitly as well. It's just not
| a very reliable mechanism. That is, imagine your code
| breaking after an update, because Lean suddenly can't
| deduce `a >= b` automatically for you anymore.
|
| >Which is fine... BUT they then should have said "so
| we're going to define a more convenient operator which is
| LIKE subtraction but isn't actually standard subtraction,
| and therefore we won't use the standard subtraction
| notation for it".
|
| What is a standard subtraction over natural numbers at
| all? As you know, under a standard addition natural
| numbers form a monoid but not a group.
| IshKebab wrote:
| > Lean can deduce proofs implicitly as well.
|
| Sure, but you still have to explicitly ask it to.
|
| > What is a standard subtraction over natural numbers at
| all?
|
| If you need something that is always defined then you
| have to use a non-standard subtraction (i.e. saturating
| subtraction). In other words the `-` operator should not
| work for Nat. It should require you to use `-_`.
| JuniperMesos wrote:
| 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.
| auggierose wrote:
| 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.
| IshKebab wrote:
| I strongly disagree. Static types are a huge success. The
| problem here is essentially that they named things badly.
| ux266478 wrote:
| Why do you believe that static types are ultimately a
| failure?
| JuniperMesos wrote:
| Better than simply not encoding the actual invariants you
| care about.
| kleiba2 wrote:
| _> 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.
| harperlee wrote:
| 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).
| codebje wrote:
| 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!
| harperlee wrote:
| I think Idris 2 is targeted more to programming than to
| doing math, no?
| ux266478 wrote:
| 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.
| addaon wrote:
| 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.
| ux266478 wrote:
| 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.
| hmokiguess wrote:
| 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
| iLemming wrote:
| > 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"
| pydry wrote:
| >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.
|
| It's also the deficit of code we actually use day to day
| that is actually written in lisp.
|
| I file it under the same heading as haskell - a language
| that clearly has _useful ideas_ , but...
| ux266478 wrote:
| You're using Lisp software right now!
|
| I think this is the most treacherous assumption people
| tend to make about programming languages, for a few
| reasons. One of them is that we really don't have any way
| to measure software that we actually use day to day.
|
| Think about the software controlling your local water
| treatment plant, traffic lights, the software your local
| power company relies on, the software running the servers
| you connect to, and all the servers those things connect
| to. All the infrastructure in between and the
| infrastructure's own infrastructure. Allegro Lisp's
| customers are shotgun spread in industries like
| healthcare, finance and manufacturing. They're paying for
| it, so we can infer they're using it, but can anybody
| actually name what software is written in it?
|
| If we play six degrees of separation, accounting for the
| full gamut of every single computer that does _something_
| relevant to your life no matter how distant, how much of
| that software are you actually familiar with? The fact of
| the matter is that we genuinely have no broad picture.
| There is no introspective method to find out what
| software you are relying on in your day to day life,
| almost all of it is completely opaque and implicit. To
| ask "what software do I use?" is to ask an unanswerable
| question. So to then synthesize an answer is to work with
| an unsound, unsupported, incomplete conclusion, which is
| exactly how you end up assuming you don't use software
| written in Lisp, while directly using software written in
| Lisp (HN)
|
| Of course, even accounting for the epistemic issue, the
| premise is still flawed. ATS is a language with ' _useful
| ideas, but..._ ', Haskell is an aging pragmatic kitchen
| sink. Positioning the latter as the former is almost
| comedic.
| harperlee wrote:
| I mostly program with clojure. I'd love that I could agree
| with you. For clarity I was not meaning a culture of
| improductivity (but it also applies), and more of a trait
| of the culture that is improductive, choosing to focus
| productivity on the wrong goals, such as reinventing
| everything to do it "better", "more data-driven",
| "decomplected", etc.
|
| > 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"
|
| You also need to take into account the denominator of
| "number of users", though. Clojure, with a tiny population,
| had a cambric explosion of libraries, and now we can't
| argue that those are dead on one argument, and that those
| are "done" on the next one. There is a huge fragmentation
| in the clojure world, and on small populations, that hurts.
| Case in point: SQL libraries. Korma, yesql, hugsql,
| honeysql, and those are just the popular ones. Case in
| point: spec vs. schema vs. malli. Case in point: leiningen
| vs. boot vs. deps.
|
| > 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.
|
| As we lispers like to say a lot, the syntax (or lack
| thereof) is the smallest of the issues. There is a lot of
| semantic difference between all of those (except libpython-
| clj, which does not belong to that list; but we could add
| Hy instead). That's even before starting to talk about
| library compatibility. So I'd contest whether having a
| common syntax is a major productivity gain.
| mghackerlady wrote:
| 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
| d-us-vb wrote:
| Forth is at this point more of a culture than a language.
| It's a culture about keeping designs simple so that they're
| understandable. Without this, Forth is only powerful for
| programmers who can keep a lot in their heads, but lots of
| Forth programs end up being write-once. Moore's view, as well
| as most other high-level Forthers preach simplicity above
| all; a code cleanliness that would make Uncle Bob blush.
|
| Lean and most type theoretic-based languages don't merely
| preach simplicity, they demand it. A function or type with a
| handful of terms or constructors might be provably
| inhabited/total, whereas one with 2 handfuls of terms or
| constructors might not be in a reasonable amount of time due
| to the exponential growth of the proof space. Factoring code
| optimally for provability yields the simplicity that Forth
| programmers are striving for.
| iLemming wrote:
| > 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.
| patrickmay wrote:
| I came here to comment "We already have Lisp."
| DonaldPShimoda wrote:
| 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...
| mapcars wrote:
| XL is a very interesting modern iteration on extensible
| languages, unfortunately it seems abandoned.
| andai wrote:
| > 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.
| neya wrote:
| A very polite reminder that Elixir exists.
| nobleach wrote:
| The perfect programming language has: - 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.
| tizzy wrote:
| 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?
| ModernMech wrote:
| Yes, programming languages are designed for a purpose and
| importantly for a concrete system. Erlang is the way it is
| because it was designed for Ericsson's phone network. C is
| the way it is because it was designed for the PDP-11. Logo is
| the way it is because is was designed for young children. Go
| is they way it is because it was designed by Google for
| Googlers.
|
| You can't design an abstractly "perfect" programming language
| without any context. Which is why the author I think focuses
| on "perfectable", as in the language can be made perfect for
| your purpose but it's not going to be one size fits all.
| nobleach wrote:
| No, I realize that. It doesn't stop me from having my
| "perfect language wishlist". The author calling out
| "perfectable" is what got me thinking. What language would
| I choose if I were able to "perfect" it just a bit more?
| ModernMech wrote:
| But you had called your list "one size fits all".
| nobleach wrote:
| oh yeah absolutely. The moment you start blowing up Go with
| features (for example) the speed decreases dramatically.
| jerf wrote:
| "Isn't the compile speed of Go so good because it's type
| system is much simpler?"
|
| That, and forgoing fancy compile-time optimization steps
| which can get arbitrarily expensive. You can recover some of
| this with profile-guided optimization, but only some and my
| best guess based on the numbers is that it's not much
| compared to a more full (but much more expensive) suite of
| compile-time optimizations.
| matt_kantor wrote:
| One thing I like about TypeScript is that there's tooling for
| "quickly strip out the types and give me something I can run;
| I don't care if it's correct". You can run the (slower) type
| checker concurrently with that (or whenever it's convenient
| to do so), but type-checking doesn't necessarily block you
| from being able to play with runtime stuff.
|
| I understand that this workflow can't be realized in
| languages whose runtime semantics are derived from type-level
| stuff, and while that can be quite convenient I'm personally
| willing to give it up to unlock the aforementioned workflow.
| ux266478 wrote:
| 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.
| rootnod3 wrote:
| Common Lisp Is exactly that. I wish I could use it at work.
| All my personal stuff nowadays is CL only. There is no other
| choice.
| anonzzzies wrote:
| I luckily have the freedom to work with SBCL almost fulltime.
| It is a joy; shame most will never get to experience it (few
| jobs, parenthophobia etc).
| unnouinceput wrote:
| "The compile speed of Go" - Delphi starts laughing
| matt_kantor wrote:
| > 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).
| tadfisher wrote:
| Kotlin itself has opted for inline union types to represent
| error results: https://github.com/Kotlin/KEEP/blob/main/propo
| sals/KEEP-0441...
|
| The existing Result type was a mistake to expose to users,
| IMO, as it encourages exceptions-as-control-flow and error
| type hierarchies which complicate error-handling even
| further. The convenient `runCatching` API also completely
| breaks reasonable error-handling on the JVM and Kotlin's
| structured concurrency (which happens to use exceptions-as-
| control-flow to signal coroutine cancellation).
|
| Overall, Kotlin is moving away from higher-kinded types in
| the core language, not toward them.
| matt_kantor wrote:
| I'm not a frequent Kotlin user but none of that surprises
| me. My comment was asking about nobleach's imaginary
| "perfect programming language", which is clearly not
| Kotlin.
| utopiah wrote:
| - The reach of JavaScript
| jolt42 wrote:
| performance of Go - why not Fortran? type system of Kotlin -
| why not Scala/Haskell? Repl like Kotlin, why not Clojure?
| never_inline wrote:
| What do you like so much about Kotlin type system, and document
| / testing of elixir?
| speed_spread wrote:
| The type system of Kotlin? It's the same as Java + syntactic
| sugar for nullability. Don't pretend otherwise.
| tom-blk wrote:
| Very intersting, never heard of lean before tbh
| mplanchard wrote:
| 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.
| archargelod wrote:
| 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 =(
| gus_massa wrote:
| > _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.
| Mathnerd314 wrote:
| 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.
| CobrastanJorji wrote:
| > the easiest way to do anything is properly.
|
| Oh, what a beautiful world it would be if this were the case!
| jbreckmckye wrote:
| > 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!
| miniBill wrote:
| It's a fun challenge! My list is Ada Agda Assembly Awk BASIC
| Brainfuck C C# C++ COBOL Curry D Elixir Elm F# FORTRAN Gleam
| GLSL Go Haskell HCL Idris Intercal Java Javascript Objective-C
| Ocaml Pascal Pony Prolog Python R Ruby Rust Sh Sketch Swift
| Typescript Visual Basic Zig
| ua709 wrote:
| I don't usually like to appeal to authority but this time it's
| too "perfect".
|
| "There are only two kinds of languages: the ones people complain
| about and the ones nobody uses". - Bjarne Stroustrup
___________________________________________________________________
(page generated 2026-04-13 23:02 UTC)