The OP didn’t convert the stuff on the Mikan page into correct Markdown, so the above … is 1/2-gibberish, but Markdown isn’t exactly “natural” for normal people, so that’s not criticizing them, that’s criticizing the code-infrastructure which we geeks made, which only works for our-kind…

Here’s the information, presented readably:

We’re announcing Mikan [codeberg.org]: a proof assistant for cubical type theory, forked from the Agda codebase.

The Agda developers have recently proposed codifying their official stance on LLM-generated contributions: they are “concerned about the negative effects of large language models (LLMs) on many individuals, our society, and our planet”, but refuse to take any concrete action to address their own contribution to these. They have judged the hypothetical future usefulness of the slop generators as outweighing the present, very real harm being caused by the AI industry.

We understand that, over its 20 years of Git history, Agda’s implementation has evolved to cater to subsets of its user-base with very diverse, and often conflicting, needs. However, the attempts to bridge these divides (e.g. --without-K vs. --cubical-compatible) present a significant maintainership cost, and are often resented by both camps, since they present one camp with substantial performance costs, while offering the other camp no clear benefit, since code across the divide is written with very different formalisation sensibilities.

Other extensions to the type theory are kept despite known inconsistencies (sized types), or being impossible to adopt without complete vertical buy-in (cumulativity, erased cubical), or simply for backwards compatibility (--guarded/@lock). In the best cases, these features are championed by a single maintainer, and keeping them well-tested against the continuous adoption of new features is a struggle when very little code uses them.

Our plan is to focus on exactly one variant of the language (“full --cubical”), and to drop support for all the language features which are explicitly deprecated, inconsistent, or simply ill-understood in conjunction with this fragment. This will give us a solid base from which we can work to improve the experience of working on the Mikan codebase, to attack the existing correctness and usability issues with features like termination and positivity checking, and to pursue breaking improvements to the core type theory and its user interface.

Sounds, to me, like a necessary split: divide Agda into the 2 different kinds, & stop sabotaging itself…

“Fail early: fail often” the mantram that competent serial-entrepreneurs hold to ( because solving-the-wrong-problem won’t ever work and it’s the default random-result )

*Sandy Maguire has written books on Algebra-Driven Design, on Thinking with Types coding, & “Certainty by Construction” which is on Agda…

The Agda book’s link is: https://leanpub.com/certainty-by-construction

Anybody interested in getting a massive boost in understanding this stuff, who is more competent in math than I am, he’s the one to learn-from ( his work is above my current-level, unfortunately-for-me )

Maguire: https://leanpub.com/u/sandy-maguire

His Algebra-Driven Design gives one the understanding that it’s entirely-possible to prevent entire categories of bugs from an API by doing it algebra-1st.

He’s also written Polysemy, “higher order, no boilerplate, monads”, which is here: https://github.com/polysemy-research/polysemy

I just discovered he writes here: http://reasonablypolymorphic.com/

He truly gives programmers another level above the ruts that programmers often get caught in.

I hope that both Mikan & the people who write enabling-books on such things get to make our world work fundamentally better, by cracking the problems that simply can’t even be understood, by people who are busy being “lost in the weeds”.

Salut, Namaste, & Kaizen,

_ /\ _