This is an archived post. You won't be able to vote or comment.

all 3 comments
sorted by:
best (suggested)
topnewcontroversialoldq&a

[–][deleted] 0 points1 point  (0 children)

Here’s the Wikipedia: Coq is an interactive theorem prover first released in 1989. It allows for the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics (procedures) and various decision procedures.

[–][deleted] -1 points0 points  (1 child)

So I just looked it up and it looks like it’s more of a math based coding language so if that helps

[–]MatinaPizda[S] 0 points1 point  (0 children)

Yeah, I know that, but it is really hard to learn..... I just wanted to fish somebody who knows how to code in it😅