← Back to context Comment by empath75 2 days ago It isn’t but the borrow checker has a formal proof that does need mathlib. 3 comments empath75 Reply mejutoco 18 hours ago > 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". ndriscoll 2 days ago You can define whatever you actually rely on as an axiom. thaumasiotes 2 days ago 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.
mejutoco 18 hours ago > 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".
thaumasiotes 2 days ago 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.
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.