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.
A perfectable programming language
31–40 of 152 posts
Re: A perfectable programming language
#32> 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".
Re: A perfectable programming language
#33> 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.
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.
Re: A perfectable programming language
#34Fortran, 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 ..."
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..)
Re: A perfectable programming language
#35clojure exists as an example of people trying types and then realising it's cruft and not needed.
Re: A perfectable programming language
#36this 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
Great post. Thanks!
Re: A perfectable programming language
#37> 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…
Well Ruby kinda brought forth Crystal which while its own Programming Language is kinda Ruby but with Types.
Re: A perfectable programming language
#38> 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…
> 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.
Re: A perfectable programming language
#39The 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)
Nope! Both give 0.
Re: A perfectable programming language
#40> 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.