A perfectable programming language

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

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.

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

> the easiest way to do anything is properly.

Oh, what a beautiful world it would be if this were the case!

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.

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.

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

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

I've been messing around with a computer algebra simplifier in Lean:

https://github.com/dharmatech/symbolism.lean

Lean is astonishingly expressive.

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

XL is a very interesting modern iteration on extensible languages, unfortunately it seems abandoned.

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 like this website, it shows documentation when hovering the code while i see similar stuffs really rare in web blog areas

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.

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.

Very intersting, never heard of lean before tbh

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.

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

wait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?

A very polite reminder that Elixir exists.

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

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)

Nope! Both give 0.

>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension,

Lol

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.

[dead]

clojure exists as an example of people trying types and then realising it's cruft and not needed.