>>>>> "AR" == Alexandre Rademaker <[email protected]> writes:
> It's not trivial, but I'd like to see the ledger fully formally verified. I would love this too. First, we need a formal semantics are what a ledger actually *is*. One thing that makes Ledger easier to formally verify is that it’s always a pure function from inputs to output, so we need to define the category of inputs, and the category of each of the outputs, so that we can always know whether an output exists within the space of what is allowed by the corresponding input. I’ve done some drafting of ideas around this before, a few times in fact, but never got to the point of writing code yet. Rocq is my preferred prover, but I’m also interested in Lean these days. John -- --- You received this message because you are subscribed to the Google Groups "Ledger" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/ledger-cli/m2qzpaceug.fsf%40hera.lan.
