The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign)

Liste des GroupesRevenir à s logic 
Sujet : The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign)
De : janburse (at) *nospam* fastmail.fm (Mild Shock)
Groupes : sci.logic
Date : 15. Jul 2025, 18:01:18
Autres entêtes
Message-ID : <10561gu$2953g$1@solani.org>
References : 1 2 3 4
User-Agent : Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:128.0) Gecko/20100101 Firefox/128.0 SeaMonkey/2.53.21
Hi,
1. Everybody’s a programmer now
    The barrier to entry dropped dramatically — you can
    become a "developer" with a few online tutorials
    and a GitHub account.
2. Everybody’s an academic now
    Academia expanded, but standards often fell. In
    some places, it's publish or perish, so paper
    mills and fake research flourish.
3. Signal Collapse ↔ Systemic Uncertainty
    Credentials lose meaning, No reliable markers of
    skill, Fragile systems built on shallow knowledge
4. Signal Collapse ↔ Systemic Uncertainty
    Quantity overwhelms quality, Important truths get
    buried, Bad signals drown good ones
Etc..
Bye
Mild Shock schrieb:
Hi,
 Having 2544 issues is probably a bad sign.
I find this many issues here:
 https://github.com/rocq-prover/rocq/issues
 Mostlikely 90% of the issues can be move to
the new discussion feature of GitHub.
 LoL
 Bye
 P.S.: Same holds for Scryer Prolog with 406 issues.
 Mild Shock schrieb:
Hi,
>
Maybe AGI should take over proving.
Just take the humans out of the loop
of any programming, it leads to nowhere.
>
Bye
>
Julio Di Egidio schrieb:
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
>
>
 

Date Sujet#  Auteur
10 Jul 25 * Coq/Rocq and how to completely break it5Julio Di Egidio
10 Jul 25 `* Re: Coq/Rocq and how to completely break it4Julio Di Egidio
15 Jul17:31  `* Maybe AGI should take over proving (Was: Coq/Rocq and how to completely break it)3Mild Shock
15 Jul17:34   `* Having 2544 issues is probably a bad sign (Was: Maybe AGI should take over proving)2Mild Shock
15 Jul18:01    `- The Signal Collapse gives us System Uncertainty (Was: Having 2544 issues is probably a bad sign)1Mild Shock

Haut de la page

Les messages affichés proviennent d'usenet.

NewsPortal