Python

1921 readers

1 users here now

A community for talking about the Python programming language.

founded 1 year ago

MODERATORS

[email protected]

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

submitted 5 months ago by [email protected] to c/[email protected]

4 comments fedilink hide all child comments

top 4 comments

sorted by: hot top controversial new old

[–] [email protected] 8 points 5 months ago (2 children)

I’m sorry, what is it called?

[–] [email protected] 3 points 5 months ago* (last edited 5 months 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.

[–] [email protected] 3 points 5 months 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?

[–] [email protected] 1 points 5 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.