Zulip Chat Archive

Stream: maths

Topic: Software verification


view this post on Zulip Miguel Raz Guzmán Macedo (Nov 24 2019 at 19:21):

Does anyone know how I would start verifying a code from another language in Lean?
Say a Runge Kutta method?

view this post on Zulip Simon Hudon (Nov 24 2019 at 19:35):

The first step would be to write a Lean function that does what your code does and prove the properties you're interested in about your Lean function. There's another part which is relating the Lean function to your code but that's a long story

view this post on Zulip Miguel Raz Guzmán Macedo (Dec 05 2019 at 17:20):

So there is a 1. Reimplement the code in lean 2. Prove it does what you want.

What is the 3. Relating the lean function part?

view this post on Zulip Andrew Ashworth (Dec 05 2019 at 17:25):

program extraction (i.e. compiling lean code to your language of choice). there you must trust the compiler to do things correctly, it is a big undertaking to prove that correct.

alternatively, call the lean function that you proved correct from your language, and let the Lean virtual machine execute it. You're trusting the VM implementation then

view this post on Zulip Andrew Ashworth (Dec 05 2019 at 17:26):

alternative #3: create a model of your programming language in Lean, and then write your function in your programming language and prove things about it (in lean)

view this post on Zulip Simon Hudon (Dec 06 2019 at 20:36):

addendum to alternative #3: this might involve writing a parser for your language in Lean to create Lean definitions to correspond to your program.


Last updated: May 19 2021 at 02:10 UTC