*To*: "N. Raghavendra" <nyraghu27132 at gmail.com>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] How to verify properties of simple SML programs*From*: Jakub Kądziołka <kuba at kadziolka.net>*Date*: Sat, 02 Oct 2021 11:20:12 +0200*Authentication-results*: cam.ac.uk; iprev=pass (otis.linlux.net) smtp.remote-ip=65.21.219.100; spf=none smtp.mailfrom=kadziolka.net; arc=none*In-reply-to*: <87lf3cfttd.fsf@gmail.com>

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

**Follow-Ups**:**Re: [isabelle] How to verify properties of simple SML programs***From:*N. Raghavendra

**References**:**[isabelle] How to verify properties of simple SML programs***From:*N. Raghavendra

- Previous by Date: [isabelle] How to verify properties of simple SML programs
- Next by Date: Re: [isabelle] How to verify properties of simple SML programs
- Previous by Thread: [isabelle] How to verify properties of simple SML programs
- Next by Thread: Re: [isabelle] How to verify properties of simple SML programs
- Cl-isabelle-users October 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list