One difference with Coq is that in Coq everything is constructive. A proof of a ... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		Jaxan on Oct 30, 2017 \| parent \| context \| favorite \| on: F* – An ML-like functional programming language ai... One difference with Coq is that in Coq everything is constructive. A proof of a precondition is an object and has to be constructed in F* you could use classical logic, things are proven by a solver. (I might be wrong.)

johncolanduoni on Oct 30, 2017 [–]

You can add the law of excluded middle in Coq like you can in F*, but it would put you at odds with almost all Coq code.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact