asciilifeform: i.e. 'magic haskell oracle pronounced that my proof is proofy-enuff. nao gimme tenure.'
asciilifeform: spyked: the authors of these wonders, have very other goals in mind than to help you understand. quite the opposite.
asciilifeform: i do not have anything against mechanized proof per se. but in practice it is in ~100% of published cases used as an attempted 'i can't believe it's not self-evident correctness!' margarinesque substitute for fits-in-head.
asciilifeform: the premier peddlers of this type of snake oil 'commercially' (i.e. fattened on lavish usg contracts) are the cryptol people. they've spawned, unsurprisingly, shoddy imitators.
asciilifeform: http://btcbase.org/log/2018-04-11#1796216 << that's because the 'field' is a rat's nest of deliberate, obscurantist claptrap. 'there is no there, there.' can burn considerably more than 4y, it is a bottomless pit -- a kind of mechanized astrology.☝︎
asciilifeform: ckang: a correct program stays correct after million yrs of 'research' by butthurt usg. an incorrect one -- is incorrect immediately, even if no one 'researched'
asciilifeform: ckang: this is a fundamentally african approach.
asciilifeform: adoption can reveal presence of flaws, but not absence (tm)(r)
asciilifeform: mircea_popescu: the displacement takes place in the imagination of the usg chair warmers, naturally. 'we'll cook up this boeckian substitute, no one will have any curiosity re the real thing, when it deigns to show up' being the idea.
asciilifeform: with generous helpings of c pointerolade, opensslism, mathemadturbatorily- squigglymarked pdfolade, tall claims of 'formal verification', etc
asciilifeform: 1 caveat re 'brute force needs machine the size of 10^bignum universes running for 10^biggernum yrs' is that it presumes a flat keyspace. whereas if instead you can exclude large chunks ( because, e.g., winblowz rng is known to never output'em , or some other likewise ) ...
asciilifeform: mircea_popescu: pretty sure this is in full alignment with current paper usg.law -- recall, they stripped away immunities from shrinks, priests, wives, etc. why not also cpa.
asciilifeform: spyked: i did realize, slightly later, lol
asciilifeform: ( the operative text, so that nobody else is stuck sifting through that pile o' rubbish : ' hexchat[30394]: segfault at 7f0ca6862199 ip 00007f0ca67a5993 sp 00007ffd83fab310 error 4 in libpcre.so.3.13.3[7f0ca678b000+70000] ' )☟︎
asciilifeform: iirc there are voodoo shops with 'dollar oil'.
asciilifeform: lol that'd rock, betcha someone would buy
asciilifeform: ( for n00b readers -- folk recipe is traditional, dating to the dawn of cheap digital photo afaik, and certainly not asciilifeform's invention )
asciilifeform: how was phf's v9995-choking patch set , created ?
asciilifeform confesses to not yet grasping the mechanics of this
asciilifeform: mircea_popescu: see also^ uncleal's AFRICA2.AMS
asciilifeform: to what does a 'We create content that ranks and helps you rank' 'SEO ROI' spamatronics specialist's phone ~usually~ go ?
asciilifeform: cassidy3: this is in fact where mircea_popescu lives. you might have to wait a few hrs for him to wake up, however. meanwhile there is a log, http://btcbase.org/log , and you can read it or even speak 'into' it, he will read later at his leisure.
asciilifeform: they cost ~0 to birth. like shitcoins.
asciilifeform: douchebag: and i know some people who pwned ants with magnifying glass. incl. myself. i was 4 y.o., wat.
asciilifeform: pen-source Twitter-like experience for the masses' << ahahahawaat
asciilifeform: '...a re-implementation of the GNU Social codebase, which itself is ... an implementation of the OStatus protocol, originally forking from the GNU FM project and later merging with the StatusNet and FreeSocial projects, from the same people behind Identi.ca, which was later folded into pump.io, which uses the ActivityStreams spec along with protocols like PubSubHubBub, Salmon, WebFinger, and Atom syndication to deliver a federated, o