Elektrine lite

← Feed

Corbin

corbin@defcon.social

<p>We don&#39;t really know how to use computers, do we?</p><p>DMs are allowed; people like to ask me for opinions. Advice about computers is free as long as it stays within the Free Software ecosystem; otherwise, I&#39;m available for consulting.</p>

Posts

  • Post #4105985

    There&amp;#39;s no evidence for determinism, let alone superdeterminism. #physics #science

  • Post #4105984

    Copyright is the main reason that bandwidth is still expensive.

  • Post #4105983

    Memory allocation isn&amp;#39;t required to have rich large values that are passed through control flow. Memory allocation is required for a stack and call/return semantics.

  • Post #4105982

    I&amp;#39;ve seen a couple blog posts floating around that talk about what &amp;quot;technical&amp;quot; means. Their discussions are good and interesting but don&amp;#39;t directly get at the heart of the issue. To be technical is to pay attention to details. That&amp;#39;s all. A (classical) computer is a detail machine; it only operates upon bits, it only knows bits, and it only decides bits. To be technical is to try to keep pace with the computer and know details as precisely as it does....

  • Post #4105981

    &amp;quot;Attention is off by one&amp;quot; (https://www.evanmiller.org/attention-is-off-by-one.html) led to attention sinks, which in turn led to better quantized models. But it appears that both Google and Meta independently discovered it internally, didn&amp;#39;t fully document it, and didn&amp;#39;t include it in their published papers; yet the code showed up in public contributions. In particular, it seems like PyTorch&amp;#39;s version of multi-head attention has *never* been the version...

  • Post #4105980

    So, just double-checking how #Lean4 and #Mathlib work: * Lean takes 3GiB of RAM and a minute to open Mathlib * Lean requires about 10min to build itself in CI, only verifying required theorems * Verifying all of Mathlib is measured in hours * Lean&amp;#39;s kernel is untrustworthy due to junk theorems And yet I&amp;#39;m a clown for using #Metamath? At some point we ought to reconsider the type-theory fetish.