[isabelle] Codegen from Hoare logics?
Hello, I had a code generation question.
I am interested in imperative programs that are [mechanically] correct
by construction and I happened upon the "Abstract Hoare Logics" work
in the AFP. My question is: can code be automatically generated from
the commands in a Hoare triple? I am relatively new to Isabelle, but
from what I have seen, this seems to be a different situation than
generating code from a function const.
This archive was generated by a fusion of
Pipermail (Mailman edition) and