really-small-backpack-example VS Kind2

Isn’t this what Haskell’s backpack does? https://github.com/danidiaz/really-small-backpack-example

Also worth mention how module identity works in Backapck: two modules instantiated separately but with the same ingredients are "equal" and have compatible types.

Anyway, an alternative to RULES that I've explored is to put the proofs behind a module signature and compile to versions of the program, one with "real" proofs and another with unsafeCoerced ones. This avoids the danger of the RULEs silently ceasing to apply because of name changes (don't know how common is that danger in practice though).

Here's an example of how to use Backpack (instead of rewrite rules) to alternate between "normal" proofs and the ones which use usafeCoerce.

Perhaps Backpack could enable something similar to that?

While being nowhere near programmability, Cabal's common stanzas can be very useful to reduce duplication. An example.

Agreed. Even from a PLT perspective, I prefer Kind2 by the Kindelia Foundation for supporting inductive theorem proving (and hopefully some level of dependent types), as well as being faster to boot.

I agree. Keep in mind our language (Kind-Lang) does target the HVM, and it is really promising. The type-checker is the fastest among proof assistants, by far; the error messages are really nice; it has a fully dependent type system which is a breath of fresh air to work with. It is still not production ready though (mostly due to lack of IO), but is the extend of our effort on that direction. We hope other lang developers get encouraged to target the HVM to. Elm and Idris are great candidates for that IMO.

Another very small proof system: https://github.com/moonad/formcorejs

The core implementation is under 700 lines of JS, including the parser: https://github.com/moonad/FormCoreJS/blob/master/FormCore.js

The author has since moved on to building a runtime with optimal evaluation (https://github.com/kindelia/hvm) and a new proof language on top of that (https://github.com/Kindelia/Kind2) with considerably better performance than existing proof systems.