A perfectable programming language

Original Article ↗ Hacker News Discussion ↗

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.