On November 28, 2020 5:23:07 AM EST, Mario Carneiro <[email protected]> wrote: >On Sat, Nov 28, 2020 at 4:04 AM savask <[email protected]> wrote: > >> I'm a bit late to the discussion, but do I understand correctly that >this >> new community verifierfin is supposed to be a spin-off to MM0/MM1 project?
I find Mario's MM0/MM1 work very intriguing, but I'm not currently ready to entirely switch to just that. But he's done a lot of interesting work, so the question is, can we build on that somehow? One intruguing idea is doing more lower-level work in Rust. Rust is fast, it can be compiled to wasm (making it callable in a browser), and its C interface makes it callable from anything. I've started looking at Stephen O'Rear's Rust verifier with the goal of adding capabilities... and least definition checking. Having some library components in Rust could mean others could more easily write things in many languages. --- David A.Wheeler -- 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/600FFDB7-8F4A-41E9-9264-BD3A84DB2894%40dwheeler.com.
