Re: [isabelle] Codegen from Hoare logics?
Isabelle let's you generate code from inductive definitions (in certain
cases). But it will still be functional code, not imperative. And it is
unclear to me why you would need Hoare logic to generate the code. The
program already is the code (modulo unparsing it).
Luke Wagner wrote:
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