10 ms·
A perfectable programming language
- deleted 5mo ago[deleted]
- spankalee 5mo agoWhat 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.
- JuniperMesos 5mo agoI think this is just applying the same informal writing style used in, for example, online chats with friends, to a relatively-informal blog post. I don't think this has anything to do with the Bay Area or its tech industry in particular.
- deleted 5mo ago[deleted]
- losvedir 5mo agoWow, I read the whole thing without noticing that. But as someone who came of age in the AIM / ICQ / IRC days, it feels pretty normal. That's just how we wrote. I still fall into it by accident when the context is right and I'm not thinking about it (eg Slack at work). I hope youngsters aren't judging me for it.
- noosphr 5mo agowe wrote like that because each message was a single sentence if you wanted more than one sentence you sent one then wrote the other it's painful to read longform the victorians didn't give up on punctuation and regular english just because they had the telegraph
- giancarlostoro 5mo agoThe swearing is another thing I keep seeing more of.
- trueno 5mo agoi notoriously ignore using my shift key when im typing informal stuff (comments, chats to coworkers, friends, etc). big ol emails = you'll see me using my shift key. most of this comes from me noticing how funny sql looks with all the people trying to use caps all over the place as if anyones working in a place without syntax highlighting in 2026. sql is the wild west and everyones sql looks like shit there is no shame. i was told i needed to use caps more early on in sql and i lmfao'd, but i was new to the career and that scarred me. i write lower case sql just to spite others now and if you see something capitalized you know i meant it, but for the most part you have to pay me to use my shift key. my trauma is now your trauma
- binary132 5mo agoOnly you can stop generational SQL abuse. Capitalize keywords, indent grouped syntax, and use prefix commas on newlines. Write readable code, for God’s sake, you filthy heathens.
- QuadmasterXLII 5mo agoits not caused by a habit of writing authentically formatted Homestuck rp smut but surely its correlated
- bobanrocky 5mo agoYES, THIS (capitalized on purpose). Folks, please use reasonably correct writing syntax. You CAN do better .. At least think of the AIs consuming your writings.
- Joel_Mckay 5mo agoI ReSpEcTfUlLy DiSaGrEe FrIeNd -- PeOpLe LoVe SlOp. =3
- jason1cho 5mo agoIs it due to the feature that the author claimed "this blog post is itself Lean code"?
- GeoPolAlt 5mo agoIt’s to show you’re too cool for grammar rules.
- ajkjk 5mo agoIt communicates a certain tone that is sometimes what one is going for. I do it in HN comments sometimes if I'm feeling, like, dry or dismissive.
- yuppiemephisto 5mo agosome combo of implicit pride and laziness. sorry, i'll fix it up
- ilsubyeega 5mo agoi like this website, it shows documentation when hovering the code while i see similar stuffs really rare in web blog areas
- md224 5mo agoI believe you can thank Verso for that: https://github.com/leanprover/verso https://github.com/leanprover/verso
- zem 5mo agothis 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 https://kirancodes.me/posts/log-ocaml-to-lean.html
- snthpy 5mo agoGreat post. Thanks!
- travisgriggs 5mo agoFortran, 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 ..."
- riffraff 5mo agoIndeed! I got to about 20 with A-B-C but it somehow became harder after those. The multitude of C-something is obvious but I didn't realize there's so many A* languages (apl, ada, agda, alice, algol, applescript, apex, ampl, assembly..)
- cestith 5mo agoThen there’s the actual language ABC. It’s in the Basic family and has whitespace indentation for structuring flow. It directly influenced Python. You could start your list alphabetically with A, A+, and A++. A is derived from APL. A+ is a newer take on A. A++ is unrelated. https://a-plus-plus-devs.github.io/aplusplus/guide/getting-started https://a-plus-plus-devs.github.io/aplusplus/guide/getting-s...
- zero_shift 5mo agoC--! I forgot that one. The ILR for the first versions of the Glasgow Haskell Compiler
- solomonb 5mo agoi 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.
- landl0rd 5mo agoImo F* is a much better choice for proof-oriented programming than lean4. The latter is still largely about mathematics while the former has things like https://fstarlang.github.io/lowstar/html/LowStar.html https://fstarlang.github.io/lowstar/html/LowStar.html
- eggy 5mo agoYes, a strong argument, and staying in a line of PLs: F# for high-level, and F* <-> Low* for theorem proving and low-level coding. I am evaluating F/Low for verified code on Cortex M processor that I am currently trying to write SPARK2014. The Cortex A processor is running seL4 for less safety-critical tasks. I did look at Lean4 as a scratch for my Idris2 itch use cases.
- whacked_new 5mo agowait, I'm intrigued, it says the blog itself is lean code. How? It's rendered, like pollen?
- ajs1998 5mo agoIt is verso. My understanding is that it's like really fancy javadocs that makes communicating Lean code easier for everyone. https://github.com/leanprover/verso https://github.com/leanprover/verso
- heliumtera 5mo ago>The recommended way to install Lean is through VS Code and the Lean 4 VS Code extension, Lol
- adamnemecek 5mo agoIt makes complete sense to polish that usecase.
- jinwoo68 5mo agoThere are community-built editor supports. For example, - Emacs: https://github.com/leanprover-community/lean4-mode https://github.com/leanprover-community/lean4-mode - Neovim: https://github.com/Julian/lean.nvim https://github.com/Julian/lean.nvim I'm using the Emacs lean4-mode and it's pretty good.
- unexpectedtrap 5mo agoUnfortunately 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.
- c0balt 5mo agoLean is far off the most bloated one. Isabelle most likely takes that spot, the main archive includes a whole vscodium among other things.
- senko 5mo ago>> Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three. > Lean is far off the most bloated one. Isabelle most likely takes that spot. Among these three is the operative phrase here. I hate to be pedantic, but we are talking about theorem provers here :)
- c0balt 5mo agoThat is a fair point, thank you for the correction there
- pjmlp 5mo agoStatic linking wonders? Originally Lean was coded in C++, and dynamically linked executable, if I remeber correctly.
- unexpectedtrap 5mo agoNo, it’s still linked dynamically and its kernel is still in C++ (see https://github.com/leanprover/lean4/tree/master/src/kernel 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) and the other 1 GiB from a standard library. As you might guess, these files are IR and essentially a compiled Lean’s environment (something like a Lisp image), so that Lean can load them straight up without recompiling and rechecking everything. There were some proposals like compressing all the .olean files, but (as far as I know) none of them were implemented. Well, even if some proposals were implemented, their contribution was effectively negated anyway.
- xarope 5mo agointeresting 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.
- psychoslave 5mo agoAre 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.
- c0balt 5mo agoI don't know about running per se but practical applications (as in done for product/service) exist. A notable practitioner for Isabelle and Lean is AWS[0]. There is also TLA+ for a more practical tool. The most widely used variant of these proof assistants are probably formally verified compilers, like compcert, which are used in some highly regulated industries like aviation. [0]: https://isabelle.systems/zulip-archive/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Big.20news.20from.20Amazon.20Web.20Services.html https://isabelle.systems/zulip-archive/stream/247541-Mirror.... and https://lean-lang.org/ https://lean-lang.org/ (Cedar)
- dharmatech 5mo agoI've been messing around with a computer algebra simplifier in Lean: https://github.com/dharmatech/symbolism.lean https://github.com/dharmatech/symbolism.lean Lean is astonishingly expressive.
- snthpy 5mo agoVery 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.
- shevy-java 5mo ago> 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".
- ChadNauseam 5mo ago> 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. Who else would add them, besides people who want them? I'm confused about what you're even claiming here. It sounds like you feel that there's a vocal minority of type enthusiasts who everyone else is just humoring by letting them bolt on their type systems.
- mastermage 5mo agoWell Ruby kinda brought forth Crystal which while its own Programming Language is kinda Ruby but with Types.
- danieltanfh95 5mo agoclojure exists as an example of people trying types and then realising it's cruft and not needed.
- iLemming 5mo ago[dead]
- IshKebab 5mo agoThe 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.
- unexpectedtrap 5mo agoWho said that it should be a compile time error? That’s just a convention, and this is definitely not a bad one. No one is going to like the need to pass each time a proof that `a ≥ b` for every `a - b` invocation. Taking into account that this proof will most likely be an implicit argument, that would be a really annoying thing to use. On the other hand, array indices by default do require such a proof, i.e., this code produces a compile time error: def x := #[1, 2, 3, 4] #check x[7] Kevin Buzzard even wrote a blog post about a similar question about division by zero: https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/ https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
- IshKebab 5mo ago> this is definitely not a bad one It definitely is a bad convention because it's highly surprising. That's what makes it a footgun. > that would be a really annoying thing to use Sure. So maybe provide "unchecked" versions for when people don't want to bother. We've known this about interface design for literally decades. The default must be safe and unsurprising. You need to opt into unsafety.
- unexpectedtrap 5mo ago>It definitely is a bad convention because it's highly surprising. You know that `Nat` represents non-negative numbers, and you see that `1 - 2` does not produce a compile error. What value do you expect then? What’s so surprising about choosing zero as a default value here? Do you expect it to panic or what?
- kleiba2 5mo ago> 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.
- harperlee 5mo agoThe 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).
- codebje 5mo agoThe 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!
- harperlee 5mo agoI think Idris 2 is targeted more to programming than to doing math, no?
- ux266478 5mo agoYep. I also think it's the best designed out of any of them. As dependently typed languages have become more and more popular, I find it a bit sad that Idris has stayed relatively obscure.
- addaon 5mo agoSince you've clearly looked at this a bit... would you give a sentence or two comparing Indris, F*, and the other lesser known players in this space (languages for both writing and formally verifying programs)? I find it a wide space to explore, and while ecosystem maturity seems like a huge deciding factor right now, I assume there's real and meaningful differences between the languages as well.
- mapcars 5mo agoXL is a very interesting modern iteration on extensible languages, unfortunately it seems abandoned.
- andai 5mo ago> 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.
- neya 5mo agoA very polite reminder that Elixir exists.
- vomayank 5mo ago[flagged]
- deleted 5mo ago[deleted]
- deleted 5mo ago[deleted]
- nobleach 5mo agoThe 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.
- utopiah 5mo ago- The reach of JavaScript
- tizzy 5mo agoI 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?
- ModernMech 5mo agoYes, programming languages are designed for a purpose and importantly for a concrete system. Erlang is the way it is because it was designed for Ericsson's phone network. C is the way it is because it was designed for the PDP-11. Logo is the way it is because is was designed for young children. Go is they way it is because it was designed by Google for Googlers. You can't design an abstractly "perfect" programming language without any context. Which is why the author I think focuses on "perfectable", as in the language can be made perfect for your purpose but it's not going to be one size fits all.
- nobleach 5mo agoNo, I realize that. It doesn't stop me from having my "perfect language wishlist". The author calling out "perfectable" is what got me thinking. What language would I choose if I were able to "perfect" it just a bit more?
- tom-blk 5mo agoVery intersting, never heard of lean before tbh
- mplanchard 5mo agofwiw, 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.
- archargelod 5mo agoFor 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 =(
- deleted 5mo ago[deleted]
- gus_massa 5mo ago> scheme: minimalist Lisp dialect used in academia There are very minimal versions and also huge versions with lot of libraries, batteries and the kitchen sink.
- Mathnerd314 5mo ago
- CobrastanJorji 5mo ago> the easiest way to do anything is properly. Oh, what a beautiful world it would be if this were the case!
- zero_shift 5mo ago> 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!
- miniBill 5mo agoIt's a fun challenge! My list is Ada Agda Assembly Awk BASIC Brainfuck C C# C++ COBOL Curry D Elixir Elm F# FORTRAN Gleam GLSL Go Haskell HCL Idris Intercal Java Javascript Objective-C Ocaml Pascal Pony Prolog Python R Ruby Rust Sh Sketch Swift Typescript Visual Basic Zig
- siev 5mo agoHahaha I very much enjoyed seeing GOOL there. I also love that you went for that over GOAL, which is probably the much more famous one.
- ua709 5mo agoI don't usually like to appeal to authority but this time it's too "perfect". "There are only two kinds of languages: the ones people complain about and the ones nobody uses". - Bjarne Stroustrup
- nektro 5mo agobody { max-width: 70rem; }