Re: [isabelle] How to verify properties of simple SML programs

Thanks for the clarification.  I'll see the program extraction manual.



At 2021-10-02T11:20:12+02:00, Jakub Kądziołka wrote:

> The workflow of producing a verified program in Isabelle goes the other
> way around — you define the functions in your Isabelle code, and then
> instruct Isabelle to generate the corresponding code in SML, OCaml,
> Haskell, or Scala, by using the export_code command (see
> The SML_file command imports your definitions on the meta level — they
> can be used to write automation for finding the proofs, but are
> completely outside of the logic and nothing can be proved about them.
> Hope this helps.
> Regards,
> Jakub Kądziołka

N. Raghavendra <raghu at>,
Harish-Chandra Research Institute,

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