Human folly for 02021-01-15

older newer index

• Lean and Metamath zero (slawekk.wordpress.com):

  notes on #formal-methods alternatives for #foundations-of-mathematics, covering #Xena, #Kevin-Buzzard, #LEAN, and #Metamath

• (nitter.net):

  discussion of #parsing with #FSM #conservative-approximations

• Mla 841039453 noblex pprnx1a smart qube proyector portatil Android 71 jm (articulo.mercadolibre.com.ar):

  #projector #avarice $21000, 854×480, 341 g

• Mla 856877892 proyector LED potente full HD 4K HDMI VGA USB WiFi Android jm (articulo.mercadolibre.com.ar):

  #projector #avarice $34000, 2600 g, 1920×1080, #fraudulent claim of "4k"

• Wholesale battery and case (banggood.com):

  #battery #avarice #18650 cells for US$3 to US$6

• Mla 641339627 pila Samsung inr18650 25r 2500mah factura a O B jm (articulo.mercadolibre.com.ar):

  #battery #avarice 2500 mAh Samsung #18650 for AR$1100

• Mla 847064486 5 X pila bateria recarg 18650 Motoma 37v 2600mah linterna jm (articulo.mercadolibre.com.ar):

  #battery #avarice 2600 mAh Motoma #18650 for AR$670

• Mla 621014301 pila bateria recargable 18650 37v jm (articulo.mercadolibre.com.ar):

  #battery #avarice “3500 mAh” #18650 for AR$250

• Moderna coronavirus vaccine Technology how it works (globalnews.ca):

  designing the #covid #vaccine took #Moderna two days from 02020-01-11

• Street talk who owns your brain (dmagazine.com):

  Evan Brown was the #intellectual-property of Alcatel (which bought DSC). #human-rights

• Evan Brown (salon.com):

  Evan Brown lost his bid for a jury trial to keep DSC from enslaving him as their #intellectual-property. #human-rights

• (gist.github.com):

  Another inspiring #incremental #PEG #parsing sketch by Darius Bacon. #algorithms

• (gist.github.com):

  Darius Bacon’s minimal #PEG #parsing system, minimized from his full-featured system Parson

• Kleene algebra (en.wikipedia.org):

  +, non-commutative ×, and unary ★ on a set give you a "Kleene algebra" if you have associativity of + and ×, commutativity of + (alternation), distributivity, identity elements, and annihilation (0×a = a×0 = 0), giving a semiring, plus idempotence of +, an ordering, and some ordering-related properties on ★.

• Att collapse (users.csc.calpoly.edu):

  #history of when the AT&T network went down for nine hours of January 15, 1990, reducing their uptime over the lifetime of the company to five nines

• Mmverify (us.metamath.org):

  Raph #Levien’s #Metamath verifier in 300 lines of Python. #formal-methods #foundations-of-mathematics

• (arxiv.org):

  “Specifying verified x86 software from scratch” Mario Carneiro wants to prove a #Metamath verifier correct with #Metamath. #foundations-of-mathematics #formal-methods

• Item (news.ycombinator.com):

  discussion of #Metamath Zero. #foundations-of-mathematics #formal-methods

• (pqdtopen.proquest.com):

  azonenberg’s "Antikernel" dissertation about moving the microkernel #security features into #hardware

• Item (news.ycombinator.com):

  discussion of (MIT) Li et al.'s #graphics rasterizer that’s differentiable (because it uses a sigmoid where normal rasterizers would use a step function) for #optimization

• (subtext-lang.org):

  the new site for Jonathan Edwards’s #subtext programming #language

• (nitter.net):

  Mt. Gox #Bitcoin bankruptcy

• Mla 901140266 HP Pavilion 14 v009la 16 GB de RAM AMD A10 5745m quad core jm (articulo.mercadolibre.com.ar):

  the laptop I bought: used “Hp Pavilion 14-v009la 16 Gb De Ram. Amd A10-5745m Quad Core, HP 14-v009la, 16 GB RAM, 700 GB disk, 1366 x 768, AMD Radeon R7 M260, AMD A10-5745. 1.94 kg, HDMI, 3 puertos USB, cámara web: 1 Mpx, Ancho: 345.4 mm, Profundidad: 241.5 mm, Altura: 23.9 mm”

• 2021 01 05 spellchecker (zverok.github.io):

  someone wrote an “explanatory” Hunspell rewrite called Spylls in 1500 lines of Ruby.

• Planckforth (github.com):

  Planckforth is a #smallisbeautiful #bootstrapping #Forth bootstrapped from a handwritten 1KB ELF binary. #source-code