Mastodon Feed: Post

Mastodon Feed

Boosted by dysfun@treehouse.systems ("gaytabase"):
amy@types.pl ("Amélia Liao") wrote:

We're announcing Mikan: a proof assistant for cubical type theory, forked from the Agda codebase.

Note: you can also read this announcement as a Gist.

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.

Signed: