XPost: sci.logic, comp.theory   
   From: janburse@fastmail.fm   
      
   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)