Translation of Python code to Coq | Formal Land

2 years ago by freewifi to c/python

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.

NegativeLookBehind 8 points 2 years ago

save

path: 0 10069762, hotness: undefined, score: 8, children: 2

sugar_in_your_tea 3 points 2 years ago

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.

save

path: 0 10069762 10070423, hotness: undefined, score: 3, children: 0

rutrum 3 points 2 years ago

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?

save

path: 0 10069762 10073304, hotness: undefined, score: 3, children: 0

rutrum 1 point 2 years 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.

save

path: 0 10074020, hotness: undefined, score: 1, children: 0

python

@sh.itjust.works

A community for talking about the Python programming language.

go to feed...

python

@sh.itjust.works

A community for talking about the Python programming language.

go to feed...