Sujet : Re: Coq/Rocq and how to completely break it
De : julio (at) *nospam* diegidio.name (Julio Di Egidio)
Groupes : sci.logicDate : 10. Jul 2025, 13:31:14
Autres entêtes
Organisation : A noiseless patient Spider
Message-ID : <104obqh$r4na$3@dont-email.me>
References : 1
User-Agent : Mozilla Thunderbird
On 10/07/2025 14:01, Julio Di Egidio wrote:
The end of the world is nigh:
<https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/status.20and.20future.20of.20the.20phase.20split/near/528029103>
From interactive proof assistant to completely upside-down and
completely broken, and not just on that at that point of course.
And the fucking shamelessness...
But we must thank MS for the nail in that coffin, too: they can't
be satisfied with just a Lean broken by design, they must own the
whole compartment: only poisoned meatballs for the public...
-Julio
Coq/Rocq and how to completely break it
The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign)