On Sat, Nov 21, 2020 at 7:10 PM vvs <[email protected]> wrote: > Rust isn't a functional programming language, but the first implementation >> of MM1 was in Haskell and it had some memory usage and speed issues that >> would have required some significant concessions to imperative style to fix. >> > > Too bad for Haskell I'd guess. I don't think that there is no solution, > here's how Lean 4 deals with similar problem: > https://arxiv.org/abs/2003.01685 >
Yeah, I was somewhat involved in the research behind that paper. I think it's trying too hard to fit imperative style into a proofy language; it's difficult to be direct with that approach and there are certain kinds of constructions that are impossible with it (like getting the value you store in a pointer-keyed hash table back out later). You still need a good compiler to make the code efficient - this was a big problem in lean 3 and lean 4 is solving it at great development expense. Here I think we do better to just let the established programming languages do what they were designed to do. Research on a provably correct programming language is an entirely different matter, which I am working on ( https://github.com/digama0/mm0/blob/master/mm0-rs/mmc.md), but it's really a separate question from a proof assistant, which is just a regular program to help people write proofs. > -- 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/CAFXXJSsu%2B14SmXjmoOWLRL4uCkFy1drOR2Qcxo6P1640E%2BJbJA%40mail.gmail.com.
