Python @sh.itjust.works freewifi @sh.itjust.works 6mo ago

Translation of Python code to Coq | Formal Land

formal.land Translation of Python code to Coq | Formal Land

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.

4 comments

I’m sorry, what is it called?
- Coq. They just want to Python and Coq interchangeably so they can prove their Python/Coq is free of bugs. It's just a way to get your Python/Coq tested to ensure it's clean to use, and ideally it would be tested frequently.
- Its pronounced "coke" I believe. Its named after the french mathematician Thierry Coquand. Apparently coq is also a name for rooster. According to wikipedia, computer science in France frequently names things after animals? Idk dont we all?
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.