← Back to context

Comment by empath75

2 days ago

I am currently working on a language compiler in lean and it seems to be fine, but compilation times are horrific and having a mathlib dependency just to build a programming language is a big ask for people.

OTOH, my borrow checker is provably sound, which is why I am using it.

6 comments

empath75

Reply
mejutoco  2 days ago

I dont think mathlib is mandatory to use lean.

  • empath75  2 days ago

    It isn’t but the borrow checker has a formal proof that does need mathlib.

    • mejutoco  10 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.