Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A perfectable programming language

alok.github.io

Post reply on HN
Print view View original

111–120 of 152 posts

Re: A perfectable programming language

#111

Post by anonzzzies »

ux266478 wrote: post #79
nobleach wrote: post #59

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,…

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

Re: A perfectable programming language

#112

Post by IshKebab »

auggierose wrote: post #50
IshKebab wrote: post #39

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 subtra…

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.

I strongly disagree. Static types are a huge success. The problem here is essentially that they named things badly.

Re: A perfectable programming language

#113

Post by ux266478 »

auggierose wrote: post #50
IshKebab wrote: post #39

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 subtra…

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.

Why do you believe that static types are ultimately a failure?

Re: A perfectable programming language

#114

Post by harperlee »

iLemming wrote: post #87
harperlee wrote: post #66

Earlier quoted context omitted.

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

> 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 bac…

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.

Re: A perfectable programming language

#115

Post by tadfisher »

matt_kantor wrote: post #96
nobleach wrote: post #59

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,…

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

Kotlin itself has opted for inline union types to represent error results: https://github.com/Kotlin/KEEP/blob/main/proposals/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.

Re: A perfectable programming language

#116

Post by JuniperMesos »

auggierose wrote: post #50
IshKebab wrote: post #39

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 subtra…

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.

Better than simply not encoding the actual invariants you care about.

Re: A perfectable programming language

#117

Post by DonaldPShimoda »

kleiba2 wrote: post #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.

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

Re: A perfectable programming language

#119

Post by jandrese »

unexpectedtrap wrote: post #19

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…

The name is amusingly ironic now.

Re: A perfectable programming language

#120

Post by zero_shift »

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

Post reply on HN