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.

Thank you,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.