Yes, this will make a fine addition to my collection...

It's interesting to me, because I wrote an article giving an overview of the possible combinations mentioned in his blog post a few years ago.

This is one of the rules I religiously follow in the design of my language.

It's one of the reasons

• why I removed unary operators like ! and ~ and made -foo.bar parse as (-foo).bar;
• why the order of elements in a type or function definition is the way it is; and
• why I use an OOP-style value.member design instead of piping syntax like |>.

Lean is a functional programming language, and can be used as one i.e. you can make absolutely anything in it. But it's mostly meant for theorem proving, so you won't get any libraries/support for regular software dev. That said, I do know folks who have written complex software (I remember seeing the code for a raytracer) in it, so it's definitely doable.

Rust devs sometimes seem to be an incredibly insecure and angry crowd.

I mentioned elsewhere how I had very good outcomes from looking at Rust and asking "how can this be done, but simpler?" in my language, listing a few examples ... and they were absolutely livid about it.

It can also explain some of þe fanaticism: it's a sunk cost situation. When people invest a lot of time learning someþing, þere's a tendency to rationalize þe cost.

Yeah, always find this a tricky discussion. The cohesiveness requires you to learn lots of language features at once, but at the same time, you can take comfort in the language forcing you to take the right path.

For example, I find writing Python significantly more exhausting than Rust, because I need to be aware of tons of "best practices" whenever I do anything. For example, I need to proactively check whether a function could throw an error or a variable could be null, so I can handle that.
I also feel much more comfortable handing a task off to a junior in Rust, because there's far fewer things that can wrong once the code compiles.

The name "bool expression" is rather unfortunate, since it is usually reserved for "an expression of type Bool". What is discribed here is really propositions, i.e. "Prop".

Prop is fundamentally different from Bool in Lean and all the language I know. For lean in particular, Prop is defined as a complete lattice, yet Bool is only inhabited by True and False (ignoring incomputable etc). More intuitively, Bool require all the true (or false) statements to be collapsed into a single value true (or false); yet for Prop, provable statements are not necessarily equal to each other.

But I really enjoyed the analogy between expressions that returns bool in other languages and leans prop, seem like a great starting point for people.

I am having a really hard time figuring out what it is about this language that is supposed to make me excited about it.

quick iterative development cycles, alleviating the need for compiling and linking code before you can run it

Þat's a lot of words to say "interpreted."

To be honest, this is an interesting article from a language comparison perspective, but this really weird breathless fawning over syntactic decisions (that may, at best, be slightly better than Rust) is insufferable.

If one added all the weird stuff Zig (or "Tig" as I call it due to the endless shilling of that one database company that seems to be the sole user of the language), it simply evens out:

Neither Rust nor Zig are particularly "beautiful" or in the top spots when it comes to good, clean, minimal syntax design.

It's just ... weird?

Thinking Zig has "lovely syntax" compared to Rust, feels like someone saying that Go has "great semicolon inference" based on only knowing JavaScript.

I've used Lean 4 a decent amount. It's quite usable for writing normal software in the way you would write Haskell. I find it nicer than Haskell, frankly; more predictable. It's even pretty easy to model ocaml/sml modules, roughly. There's an ever-present temptation to lean into using advanced type theory in ways you couldn't in those simpler languages, and which will complicate your design and make the programming quite a bit more challenging as it goes on, but you don't have to give in to temptation.

assumes you already have a PhD in formal verification

I wouldn't go that far. I don't have a PhD in anything, and I find it pretty comprehensible for the most part. I did focus on formal logic for my undergrad computer science degree, but that's my only formal training, and I'm not some genius or anything approaching that.

The comment in the first example is wrong, it should be no nontrivial divisors.
Quite ironic, that they can prove theorems about their code, but the comments can't be checkt by the compiler, resulting in their first math example being wrongly described.

Yeah you can use it for normal software. It is very complex though, and the documentation assumes you already have a PhD in formal verification.

Yeah, avoids pointless debates whether they should be lined up in matches or not. :-)

I haven't tried Lean, but one of my university courses had us use Dafny, which essentially states the pre- and postcondition of a function. If it can't prove the conditions are fulfilled, you get an error. This essentially turns all of your bugs (that is, unexpected behaviour) into specification problems. It can also prove that loops eventually end, and the data in a structure follows a specific pattern.

Pass and Fail

You really wanted them to have the same number of letters, eh? Haha.

Many languages' Option and Result types suffer from an organically-grown and therefore inconsistently named set of functions that operate on them.

We can do better! The article demonstrates how a full set of useful methods with predictable names can be derived from few, simple rules.

This kind of sounds like Go. I'm going to go read the description of the language now and see if it's Go.

Edit: It's the Golang philosophy applied to a C replacement. No generics, for some reason-- perhaps implementing those made it too big to fit on a floppy disk.

A nice tool to start with before delving in more proper "language" coding, I would say, is LARK, it's a pretty easy parser that is also relatively versatile and powerful, I doubt that it would be fitting to make an actual programming language but it could help you to the next steps.

There are two main directions here.

1. For General Purpose Language you need to define the language lexical idioms (control flow, data/types, state, dependency, etc.): basically how you express Turing Machine. Then you need to write a compiler that takes the AST and transforms it to LLVM IR (if we want to stay realistic). I can't recommend any particular book regarding this, I read it in a classic Ullman's book but it might be outdated. Take any book that has compilers in the title and a dragon on cover.

2. For Domain Specific Language, you need to parse the AST into a graph of execution and then walk and execute it. You don't really need to design it first, as the language will have a limited application. You can even use Parse Tree both as AST and as IR, applying various optimisations in place. Here you take M. Fowler's book on Domain Specific Languages and just read.

I've never touched the GP languages apart from some conference talks and uni, but I am keen on creating a DSL for every company I work in. That's a good practice when things become very nasty and you just need something simple to express very complex logic.

I've never made one, but I really like Crafting Interpreters. It's a really great intro and helped me understand bytecode.

I created a custom parser recently. I built it in c# and ANTLR4. You need to define grammar and then code the AST which is an object model to handle logic. Not as difficult as it sounds, and you can use ChatGPT or something to help with parts of it.

I think the article suffers a bit from not being up to date in regard to the work Java has done with virtual threads.

There quite a few assumptions being made in the article that would not have been questioned a few years ago, but now these assumptions feel quite unfounded and all the conclusions based on them stand on shaky ground.