> 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".