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.
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.
reply