XPost: alt.philosophy, comp.theory   
   From: janburse@fastmail.fm   
      
   Hi,   
      
   Since coinduction and streams has matured   
   in proof assistants, I wouldn't be surprise   
   if the non-termination was mapped to questions   
      
   of productivity of a coinductive stream:   
      
   "For coinductive streams (infinite lists),   
   productivity ensures that the definition   
   actually produces an infinite object   
   one constructor at a time."   
      
   Proof tools like Agda/Coq have productivity   
   checkers. Kind of doing induction the   
   other way around... LoL   
      
   Bye   
      
   Mild Shock schrieb:   
   > Hi,   
   >   
   > The Coq proof of the value of BB(5), draw   
   > on a sub module BusyCoq. Which drew on an   
   > amazing array of programming languages:   
   >   
   > Verified implementations of Busy Beaver deciders.   
   > The computation is split into two parts:   
   >   
   > - First, an untrusted decider, written in Rust, tries to decide whether   
   > each machine halts. When it succeeds, it generates a certificate.   
   > - Then, a verifier, proven correct in Coq and extracted to OCaml, checks   
   > each certificate and makes sure that it is correct.   
   >   
   > They also use proof theoretic methods   
   > to show non-termination:   
   >   
   > A Coq theorem guarantees that if the verifier   
   > accepts a certificate, then the corresponding   
   > machine doesn't halt.   
   > https://github.com/meithecatte/busycoq   
   >   
   > Not consuming the atoms of the universe.   
   >   
   > Bye   
   >   
   > Mild Shock schrieb:   
   >> Hi,   
   >>   
   >> I am doing the wake-up call until everybody   
   >> gets ear-bleeding. It just too cringe to   
   >> see the symbolics computing morons struggle   
   >>   
   >> with connectionism. But given that humans   
   >> have a brain with neurons, it should be obvious   
   >> that symbolism and connections are just two   
   >>   
   >> sides of the same coin.   
   >>   
   >> Good Luck!   
   >>   
   >> Bye   
   >>   
   >> Mild Shock schrieb:   
   >>> Hi,   
   >>>   
   >>> 1) Classical computing = Boolean logic + von Neumann architecture   
   >>>   
   >>> For decades, all mainstream computation was built on:   
   >>> Boolean algebra   
   >>> Logic gates   
   >>> Scalar operations executed sequentially   
   >>> Memory and compute as separate blocks   
   >>> Even floating-point arithmetic was implemented on top of Boolean logic.   
   >>>   
   >>> This shaped how programmers think — algorithms expressed   
   >>> as symbolic operations, control flow, and discrete steps.   
   >>>   
   >>> 2) AI accelerators break from that model   
   >>>   
   >>> Modern accelerators — GPUs, TPUs, NPUs, and custom matrix   
   >>> engines — use a different computational substrate:   
   >>>   
   >>> Instead of Boolean logic:   
   >>> → Bulk linear algebra over vectors/tensors   
   >>>   
   >>> Instead of instruction-by-instruction control:   
   >>> → Dataflow graphs   
   >>>   
   >>> Instead of sequential compute on registers:   
   >>> → Massively parallel fused-multiply-add units   
   >>>   
   >>> Instead of manually orchestrated loops:   
   >>> → High-level declarative specs (XLA, MLIR, TVM)   
   >>>   
   >>> Have Fun!   
   >>>   
   >>> Bye   
   >>>   
   >>> Julio Di Egidio schrieb:   
   >>>> On 30/11/2025 22:21, Mild Shock wrote:   
   >>>>   
   >>>>> In the coming age of analog computing,   
   >>>>> symbolic logic means nothing:   
   >>>>   
   >>>> "In the coming age of analog computing" is a counter factual,   
   >>>> but if it did mean anything, it would mean the exact opposite   
   >>>> you apparently think it means: as I was saying, indeed analogic   
   >>>> does naturally go with symbolic, of course, not the other way   
   >>>> round, you other resident piece of nazi-retarded spamming shit.   
   >>>>   
   >>>>> “The high data-rate sense perception and   
   >>>>> identification abilities of the human system   
   >>>>   
   >>>> Sure.  Get the fuck out of here, you and your employer.   
   >>>>   
   >>>> *Plonk*   
   >>>>   
   >>>> Julio   
   >>>>   
   >>>   
   >>   
   >   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)