71–80 of 152 posts
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.
I 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.
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,…
I 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?
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.
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 a…
There are very minimal versions and also huge versions with lot of libraries, batteries and the kitchen sink.
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 subtra…
Who 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 c…
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.
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.
> 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.
The 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).
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 ..."
Indeed! 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..)
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-s...
Earlier quoted context omitted.
Who 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 c…
> 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.
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?
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,…
In many of these other categories, clisp exceeds requirements. The REPL and Doc situation is so good it's honestly worth it for those alone. People put up with `):'(,@ soup for good reason.
Earlier quoted context omitted.
The 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).
The 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 w…