HN

Comments (100)

• Menu

  kleiba2
  > 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.
• Menu

  unexpectedtrap
  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.
• Menu

  solomonb
  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.
• Menu

  nobleach
  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 still dream about this "one size fits all" language.
• anon
  undefined
• anon
  undefined
• anon
  undefined
• Menu

  psychoslave
  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.
• Menu

  travisgriggs
  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, SmalltalkFun challenge. Unlike the author, I have nothing really to add.I just wanted to say that "I did NOT write it with ..."
• dharmatech
  I've been messing around with a computer algebra simplifier in Lean:https://github.com/dharmatech/symbolism.leanLean is astonishingly expressive.
• Menu

  zem
  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
• Menu

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

  archargelod
  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 =(
• tom-blk
  Very intersting, never heard of lean before tbh
• mapcars
  XL is a very interesting modern iteration on extensible languages, unfortunately it seems abandoned.
• snthpy
  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.
• xarope
  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.
• andai
  > 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.
• Menu

  shevy-java
  > languages without types tend to grow them, like PHP in 7.4 and Python type annotationsWell ... 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".
• Menu

  whacked_new
  wait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?
• neya
  A very polite reminder that Elixir exists.
• Menu

  IshKebab
  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 subtraction should not give a `Nat` unless the first argument is definitely more than the second.Nope! Both give 0.
• Menu

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

  spankalee
  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.
• vomayank
  [dead]
• Menu

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