On Sun, May 9, 2021 at 12:24 PM Benoit <[email protected]> wrote:
> On Friday, May 7, 2021 at 5:20:47 PM UTC+2 [email protected] wrote: > >> (and if it is to eventually be verified it is probably best to keep it >> bare bones) >> > > Isn't it possible to verify only the core of a given program ? > Yes, although you still need the verifier to contain extra state that is ignored for verification purposes. It makes the proofs slightly more cumbersome than they would be with a bare bones verifier but not significantly so. I'm already doing a bit of that in the last few commits, since I want to use the verifier also as a plain parser (rather than the verifier version that consumes all input as soon as it understands it and never produces an actual AST). -- 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/CAFXXJSsGTWzaB9-rG8tLZs0JFP-ZYzPhZ5LfW6KAXd0spTAyJw%40mail.gmail.com.
