Not a very productive contribution to the discussion, but I'm posting it anyway: as someone who is still relatively new to ITPs but investing a lot of my spare time into Lean for maths, I find this idea very exciting. I have been writing rust professionally for a long time, and I also think it would be a good, practical implementation language. Also agree on the sentiment about writing a text editor. Definitely interested as a user and maybe more.
[email protected] schrieb am Samstag, 21. November 2020 um 04:30:36 UTC+1: > On Fri, Nov 20, 2020 at 10:22 PM Raph Levien <[email protected]> wrote: > >> 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. >> > > Yes, I'm aware of the Xi editor and my comment wasn't at all meant to > throw shade on it! I think it's a cool project, and from the demos I've > seen it looks pretty slick, if a bit raw (I don't know how much it has > progressed in the meantime). But I'm sure you can attest that it's not a > job for the faint-hearted! Of course if the *goal* is to build a good text > editor then it's a feasible project, but building a good text editor and > also a good proof assistant at the same time is probably a poor separation > of concerns. > > 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 >> >> <https://groups.google.com/d/msgid/metamath/CADBEgNPr7K5F10F0A8OVjk%2BFvdaZL6w5Q4o5KzTZB%2B4oaVaCOQ%40mail.gmail.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/a2ed06af-9ff7-44a8-9f6d-db1ba9921ff1n%40googlegroups.com.
