A perfectable programming language • Hacker News Board

Re: A perfectable programming language

#61

Post by tom-blk » Mon, Apr 13, 2026, 12:42 PM UTC

Very intersting, never heard of lean before tbh

Re: A perfectable programming language

#62

Post by pjmlp » Mon, Apr 13, 2026, 12:44 PM UTC

unexpectedtrap wrote: post #54

pjmlp wrote: post #45

Earlier quoted context omitted.

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

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) a…

Thanks for the overview.

Re: A perfectable programming language

#63

Post by mplanchard » Mon, Apr 13, 2026, 12:45 PM UTC

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.

Re: A perfectable programming language

#64

Post by tizzy » Mon, Apr 13, 2026, 12:45 PM UTC

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

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?

Re: A perfectable programming language

#65

Post by archargelod » Mon, Apr 13, 2026, 12:46 PM UTC

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 =(

Re: A perfectable programming language

#66

Post by harperlee » Mon, Apr 13, 2026, 12:55 PM UTC

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.

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

Re: A perfectable programming language

#67

Post by [deleted] » Mon, Apr 13, 2026, 1:03 PM UTC

archargelod wrote: post #65

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

[deleted]

Re: A perfectable programming language

#68

Post by [deleted] » Mon, Apr 13, 2026, 1:04 PM UTC

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

[deleted]

Re: A perfectable programming language

#69

Post by mghackerlady » Mon, Apr 13, 2026, 1:08 PM UTC

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.

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

Re: A perfectable programming language

#70

Post by codebje » Mon, Apr 13, 2026, 1:13 PM UTC

harperlee wrote: post #66

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.

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

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!