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.
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.
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.
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.
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".
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.
actually i think syntax is incredibly important, but i think i'm approaching it from a viewpoint that's even more syntactic than lisp macros, which in practice tend to center around parens syntactically still. racket a notable exception (and good, but not perfectable lang, one of the inspirations for my remark). typed racket is good but is not culturally central enough. but yeah, i do believe types are [inevitable](https://www.youtube.com/watch?v=0AQdSZqGXz4)
syntax matters for normal ppl even more than semantics in some ways since semantics can be optimized and refined on the backend, but everyone is (de)limited by their vocabulary
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.
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).
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.
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.
> 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.
- 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.
48 comments
[ 3.1 ms ] story [ 64.0 ms ] threadFun challenge. Unlike the author, I have nothing really to add.
I just wanted to say that "I did NOT write it with ..."
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.
Lol
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.
https://github.com/dharmatech/symbolism.lean
Lean is astonishingly expressive.
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.
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".
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.
Highly recommended!
https://reservoir.lean-lang.org/@strata-org/Strata isn't done, but its goal is to let one build whole languages that can look like whatever you like. ones for little kids maybe
syntax matters for normal ppl even more than semantics in some ways since semantics can be optimized and refined on the backend, but everyone is (de)limited by their vocabulary
Nope! Both give 0.
Homoiconicity anyone? Lisp is one of the oldest high-level programming languages, and it's still around.
i talked about the lisp curse in this old paper. it's rough but explicitly mentions it
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.
[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...