[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.

Thank you,

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