A perfectable programming language

Original Article ↗ Hacker News Discussion ↗

A blog post arguing that the Lean theorem prover is a “perfectable” programming language prompts comparisons with other proof assistants and typed languages, and raises the broader question of what properties a near‑ideal language should have. Commenters weigh Lean’s strengths—expressiveness, speed, VS Code integration, tools like Verso—against drawbacks such as large distribution size, non‑obvious numeric semantics, and reliance on GitHub. The thread branches into debates over static vs dynamic typing, the importance of syntax and homoiconicity (with Lisp often cited), and wishlists for a hypothetical “one size fits all” language that balances powerful types, performance, tooling, and ergonomics.

Writing style and presentation

  • Several comments focus on the article’s lowercase-first-word style and heavy swearing.
  • Some see it as an informal chat/IM style imported into blogs; others find it painful to read in longform.
  • A few deliberately use all-lowercase as a personal or aesthetic choice; others call for more conventional grammar for readability (including for machine readers).
  • Capitalization is also described as a tone marker (e.g., to signal sarcasm or dismissiveness).

Lean tooling, docs, and distribution

  • The interactive site is praised for hover-based code documentation, attributed to the Verso system.
  • Lean is commonly installed via VS Code; some find this amusing, others say it’s sensible to polish that path.
  • Emacs and Neovim integrations are reported as solid alternatives.
  • A major complaint is Lean 4’s distribution size (≈2.5 GiB unpacked vs ~15 MiB for Lean 3), mostly due to compiled IR/environment files (.olean/.ilean/.ir).
  • Suggestions like compressing IR files have been floated but (per comments) not effectively realized. Some see this as bloat and a regression.

Lean’s role among proof-oriented languages

  • Lean 4 is praised as an expressive, high-quality functional language; some want it to eventually replace Haskell for typed FP in production.
  • Others feel its “perfectability” is limited by non-constructive axioms in the standard library.
  • F* is recommended as more practical for proof-oriented programming and low-level verified code; Agda and Idris2 are preferred by some for “mathy” or program-oriented dependent types.

Types, safety, and language evolution

  • There is debate over the claim that dynamically typed languages “tend to grow types.”
  • One side stresses that all values already have types; exposing them helps tooling and linters, explaining trends in PHP/Python.
  • Others argue this is driven by a vocal pro-type minority and that type advocates understate trade-offs.
  • Some note dynamic languages accreting static features, while static languages rarely move toward dynamism.

Semantics surprises and Lean “footguns”

  • Examples: converting 256 to UInt8 and subtracting 4 - 5 : Nat both yield 0 instead of compile-time errors.
  • Critics call this surprising and unsafe; they want safe-by-default operations with explicit “unchecked/saturating” variants and distinct notation.
  • Defenders argue these total, saturating/wrapping semantics are reasonable defaults and avoid burdensome proof obligations for every subtraction, while strict proofs are still possible where needed.
  • This is used both as criticism of Lean’s API design and as a discussion of the practical limits of encoding invariants in types.

Lisp, homoiconicity, and culture

  • Some equate Lean’s “perfectable” self-description with Lisp-style homoiconicity.
  • The “Lisp Curse” (power causing fragmentation and odd local cultures) is raised; others counter that modern Lisp ecosystems can be highly productive and unify disparate runtimes.
  • There’s debate over how much Lisp is actually used in everyday software, with one commenter noting we lack visibility into much infrastructure code.

Dependently typed languages compared

  • Idris2 is highlighted as particularly well-designed and program-centric, with an interactive “hole-driven” workflow that feels like Haskell with stronger types and good editor support.
  • F* and similar systems integrate heavy SMT solving; commenters find these powerful but cognitively taxing for complex software because of constant context switching.
  • Lean is described as proof-goal–centric: work is framed around adjusting proof strategies and lemmas, suiting mathematics but feeling less like ordinary programming.
  • Some feel there is still no dependently typed language that is clearly aimed at everyday software development first.

“Perfect language” wishlists and trade-offs

  • One detailed wishlist combines Go’s speed and single-binary deployment, Kotlin-like types, OCaml-style result/option and pattern matching, Elixir-like docs/tests, strong REPL, and minimal transitive dependencies, without a heavy VM.
  • Others respond that such a “one size fits all” language conflicts with the reality that languages are designed for specific contexts (e.g., Go for Google-scale services, Erlang for telecoms).
  • Examples like Common Lisp/SBCL and Delphi are proposed as already meeting many wishlist items; differing opinions remain on type-system sophistication (Kotlin vs Scala/Haskell) and VM trade-offs.

Practical use and ecosystem

  • Questions arise about whether Lean and other provers run real-world businesses.
  • Replies cite use of Isabelle and Lean at a major cloud provider, and formally verified compilers (like CompCert) in regulated industries, plus tools like TLA+ for practical design work.
  • Some express fatigue with Lean 4 due to regressions (e.g., unification issues) and the default reliance on GitHub-based packaging.