I am tentatively interested, but have fairly limited free time, as I have a ton of other super-interesting research projects. I certainly agree that Rust is a great language for this.
Regarding writing an editor. I agree it's a big task and hard to do right. That said, it's also something I'm interested in. I know there's at least one other editor project on Druid (not my own), and we also have interest in unbundling our (Druid's) multiline text widget so it's possible to integrate other functionality on top of it. If you want help on specifically the Druid parts, you might be able to come by the #druid channel on xi.zulipchat.com and stir up some interest. Raph On Fri, Nov 20, 2020 at 2:31 PM vvs <[email protected]> wrote: > Whoa! And I'm already spoiled by what Leo is doing with Lean 4. The so > small core language and vastly extensible parser with an entire automation > library for building and proving formal systems using incremental > compilation with plans for interactive compiler guidance are mind blowing. > That's taking aside your own exciting MM0 work. And I only have that much > time to learn about lots of things. I'm torn already :( > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/dc7550eb-9c0b-4953-93b5-1c9640b0ffd9n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/dc7550eb-9c0b-4953-93b5-1c9640b0ffd9n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CADBEgNPr7K5F10F0A8OVjk%2BFvdaZL6w5Q4o5KzTZB%2B4oaVaCOQ%40mail.gmail.com.
