We are starting to work on a new product, coq-of-python. The idea of this tool is, as you can guess, to translate Python code to the proof system Coq.
  • rutrum@lm.paradisus.day
    1·
    6 months ago

    I like the motivation of the problem: use mathematical rigor to guaruntee something that is complex and certainty is a requirement, like crypotcurrency, is valid.