Stream: Program verification
Xi Wang (Oct 15 2020 at 20:10):
Just for fun, coded up the proof from the 1967 paper "Correctness of a compiler for arithmetic expressions" in Lean: https://github.com/xiw/arithcc
Simon Hudon (Oct 15 2020 at 20:45):
Nice! I think that could be the kind of stuff we put in the mathlib archive directory. @Rob Lewis What do you think?
Xi Wang (Oct 19 2020 at 21:21):
@Simon Hudon That would be awesome! Let me know if there's anything I can help with (splitting into smaller files, or merging the example into one file, etc.).
Simon Hudon (Oct 19 2020 at 21:43):
Are you familiar with the pull request (PR) process? You can have a look here: https://leanprover-community.github.io/contribute/index.html
It will show you have to create a version of mathlib that contains your code, it will let mathlib contributors and maintainers comment on it and suggest improvements.
Xi Wang (Oct 20 2020 at 00:43):
Thanks for the pointer!
Simon Hudon (Oct 20 2020 at 00:47):
Please let me know when you make that pull request or if you need more
Last updated: May 08 2021 at 21:09 UTC