Hacker News Reader

Publishing the proof is good, but why do you need it to build the language?

You can have one piece of software that does things, and a separate piece that proves that the things the first piece does are correct.

> having a mathlib dependency just to build a programming language is a big ask for people.

This is an implementation choice you did when implementing your programming language, if I understand correctly.

I thought of it because writing some lean lang I also had the option of adding Mathlib or keep it "bare".

You can define whatever you actually rely on as an axiom.