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.

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.