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



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




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