Haskell/Miranda use `::` instead of `:` for type signatures unlike Elm & basically the rest of the family which prioritize types being less keypresses than list cons.

Sorry, I meant "Haskell / Miranda style syntax" -- e.g. curried functions, concise syntax with little boilerplate, etc. The word type is too overloaded ;-)

> Features

It’s blank. Lots of blank gray rectangles too. Site is broken?

Yet folks are refusing to migrate off their products/services—as if it hasn’t been like this for 3 decades already.

I am doing my very small part by migrating large part of family and my employer away for a few years now. The world is better without Microslop. Buy unfortunately I know that this isn't always possible.

Please do. Poison the training.

This pile of Markdown files has the most cringe-inducing name I have seen in weeks.

Surely gstack was worse, right?

Having md files under "Languages" would be nice here.

fwiw GSD is a pretty well-established decision-making framework. The creator didn’t invent it

Naturally the Microsoft-owned language is getting the AI hype instead of the more mature options that could do this sort of work… Agda, ATS, Coq/Rocq, Dafny, Fstar, Idris, Isabelle, Why3 just to name a few.

A bit uncharitable. I'm a diehard fan of Rocq, but it's nothing unusual to see the young new hotness that is Lean continue to get the spotlight. It's not a sign of Microsoft putting its thumb on the scales, and the hype for Lean has long predated LLMs.

It's certainly less mature when it comes to verified programming, but its appeal to mathematicians (rather than formal methods experts) has earned it much respect.

You should check out the recent PR's to the Agda repo... the community is currently very divided about AI. For better or worse, the people driving the Lean project have been interested in AI for quite some time.

Am I missing something? Isn’t that the language most are using currently when looking at research at openai, google, deepseek etc?

Note that Lean doesn’t have a monopoly on verification languages. Dafney, Rocq, Why3, ATS, Agda, Idris… these all can do it too. The fact that Lean is controlled by Microsoft should cause folks pause considering how they are trying to monopolize so many other spaces… & the author works on Lean. Rather than comparing Lean to performance like OCaml/Haskell like the article does, Why3 is a superset of OCaml, Agda can compile to Haskell, & ATS2 compiles to C—rather than needing to adopt an entirely new language.

Would be super dope if they brought back headphone jack Google teased Samsung over then a year later removed entirely. I haven’t even once considered GrapheneOS since I refuse to go without basic I/O.

XML works great for XMPP. KDL is compatible with it too.

What gets me is going from this structured data to Markdown which doesn’t even have enough features & syntax that the LLMs try to invent or co-opt things like the blockquote for not quoting sources.

If it’s GPL then you must care about “free software”. If that is the case, you should reconsider hosting on a fully-proprietary code forge. It requires cognitive dissonance to thing FLOSS is the right license for your project but not for your tooling/community.

You’re projecting that you would feel cognitive dissonance if you made the same choices as OP.

It’s perfectly reasonable for people to want to license their own work under a particular license without believing that everyone else should do the same, for example. Someone with that opinion, or a whole host of other positions that allow for different licenses to coexist, wouldn’t experience any cognitive dissonance.

The question then becomes what you are going to do about your cognitive dissonance. Continue to believe that “everyone else must be wrong”?

Not the same thing to compare how others should license their software versus keeping ideals consistent in your own project+tooling. If “everyone else must be wrong”, why are there continually waves of projects leaving ever since the Microsoft acquisition in particular? There’s a correlation with the kinds of projects that left too being philosophically aligned with free software & copyleft.