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



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

Regards,
Raghu.

----------------------------------------------------------------------

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
> https://isabelle.in.tum.de/dist/Isabelle2021/doc/codegen.pdf).
>
> 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 hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/




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