Software verification

Stream: maths

[Miguel Raz Guzmán Macedo]

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

[Simon Hudon]

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

[Miguel Raz Guzmán Macedo]

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?

[Andrew Ashworth]

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

[Andrew Ashworth]

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)

[Simon Hudon]

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