asciilifeform: the die ? i dun think even today there is die whole 4mm tall

asciilifeform: mircea_popescu: i dun think he's the comic d00d

asciilifeform: mircea_popescu: i dun expect he has an ion accelerator, no

asciilifeform: SeanRiddle: i tried to look at the high res samples on your www, but found only http://btcbase.org/log/2018-11-28#1875711 ☝︎

asciilifeform: trinque: i can't speak for deedbot, but the ircbot code i put pehbot on doesn't autoreconnect at all

asciilifeform: iirc that was last one i saw ( and the only 1 in orig lang )

asciilifeform: hey i even managed to see disneys. a coupla, with the trad ru dubbing translator with clothspin on his nose going mmmm

asciilifeform: it's at least the 5th time i got that q, nearly lost count

asciilifeform: i pictured zx2c4 as also young, but i have nfi specifically

asciilifeform: it was quite similar, imho, to the gabriel laddel fella. clearly there was 'somebody home' in the crankcase, but under a thick haze of substances and detritus from indiscriminate suction of ??? from heathendom. 'salvation of the drowning is work for the selfsame drowning', what can i say.

asciilifeform: i gave ~hour to attempt to cure. in retrospect it was folly, made 0 dent.

asciilifeform: mircea_popescu: i still can't make heads or tails of wtf was in that d00d's head. shows symptoms of some kinda maths education. but omfg the 'cd-r brain'.

asciilifeform: in current-day ru, as i understand you need repeated (1 corpse generally not suffice) wetwork to merit >decade

asciilifeform: http://btcbase.org/log/2018-11-30#1876362 << i'll admit, i kept half-expecting him to actually read a ch of ffa and go 'hmm... maybe i should throw out my c hairball and mecha-proofisms' but of course no dice. ☝︎

asciilifeform: ty diana_coman ! i will sew it into ch14.

asciilifeform: i'ma bet was not acctd for in the 'proof'isms..

asciilifeform: let's bounce the rubble, also.. http://btcbase.org/log/2018-11-30#1876304 >> ftr i have iron right here where this will bomb, cuz byte not 8bit there. ☝︎

asciilifeform: i can show this because the inputs , for given size, literally do not affect the program branch flow.

asciilifeform: consider, zx2c4 , i can show that nuffin in my arithm routines can overflow a buffer. even if you were to turn ada's overflow checks off. without any complicated tooling.

asciilifeform: and i could continue..

asciilifeform: what i see in the link, is a buncha c code, with pointerisms

asciilifeform: i dun publish my 'derive' barf

asciilifeform: i'd hope that i dun have to explain that when you write a cryptosystem, you are in fact asking other people to do this.

asciilifeform: i.e. wouldja bet life of self, wives, pets, whole clan of yours, on there being no boojum in coq, z3, other claimed brain substitute of the day ?

asciilifeform: it was a misery. and 'sage' made it ~more~ of misery, if yer gonna commit 'machine proof' atrocities, has no biz doing in a non-homoiconic lang (i.e. any non lisp)

asciilifeform: zx2c4: you may find it interesting to learn that i once worked in a dour 'salt mine' where shat out 'correctness proof' all day. in 'sage.' ☟︎☟︎

asciilifeform: as it is i have less nausea for even honeopaths than for mecha-proof folks

asciilifeform: and i'm to take it seriously after that ? pray tell why ?

asciilifeform: i have not read src of coq, to do so would take 20yr ( and i dun mean 'skim', but to find total proof of correctness of whole shebang and load into MY head )

asciilifeform: zx2c4: lemme ask, on what authority am i to accept the correctness of a proof generated via e.g. coq ?

asciilifeform: zx2c4: whole reason i bother with this thread is to explain why no, i would ~not~ like to suck the coq, if you will

asciilifeform: i sometimes even use computer algebratrons, in exploratory work. but would never consider presenting output straight from one as 'here, correct'

asciilifeform: zx2c4: i like paper. and even chalk.

asciilifeform: grasp obvious in its totality, as in there is literally NO hesitation to strap the thing on and 'if mistake -- any mistake -- i hit cement at terminal velocity'

asciilifeform: the statement is quite serious, i and some yet-unknown number of other people will literally bet arse on our grasp of ffa correctness.

asciilifeform: not fits in head ? not proven. ( i did not say ~whose~ head, but imho safe to suppose that whole f# microshitiana garbage pail fits in no head )

asciilifeform: zx2c4: try to think about what i actually said tho

asciilifeform: zx2c4: point being, i don't practice haskellism. and nit from being illiterate yokel who has nfi how. it so happens that i know how. but consider the whole approach to be braindamaged .

asciilifeform: in all seriousness, i don't even presently know of a more leprous pile of shit, either on pedigree or technical pov.

asciilifeform: right. ( and as presently stands, i've abolished all but 1 of the algos where this actually takes place )

asciilifeform: on 2nd pass of log, noticed that i did not answr http://btcbase.org/log/2018-11-29#1876084 : answr is, it is for shifting ~into~ a FZ . ( if this wasn't clear from thread ) ftr. ☝︎

asciilifeform: diana_coman: i'ma also note, _O_I is used strictly in fz_mod : http://www.loper-os.org/pub/ffa/hypertext/ch13/fz_divis__adb.htm#83_14 ; prolly oughta be inlined ~there~ and abolished as a global (even internally) function.

asciilifeform: i.e. one will call, roughly, P(pcodestring, ffawidth, ffaheight, maxsteps) and get output.

asciilifeform: and in principle i'm not averse to adding detail to comments. ( this is exactly the reason why comments exist -- show what is not necessarily evident from the coad )

asciilifeform: ( the only guarantee i can offer in good conscience is that nuffin can be broken by operating the ~external~ controls -- but even there user is required to see whether his cpu has barrel shifter (see ch13 discussion) , constant-time mul ( see ch9 discussion ) )

asciilifeform: i'ma add commentary/warnings when diana_coman et al point out good additional places where; but no one should live with expectation that ~all~ possible ways to break ffa by monkeying with internals, will be listed

asciilifeform: and this is prolly not the only instance of the item. ( i discussed it briefly in ch11 , in the section where preconditions -- ended up moving many preconditions to the exported wrappers, they slow things down quite substantially when present on inner-looped invocations, as they prevent (for obv reason) inliner )

asciilifeform: diana_coman: i'ma absolutely add it to comment and discuss in ch14 mail bag.

asciilifeform: it will produce garbage, yes. i considered to make OF_in a limited type, but it would slow down the place where the item is actually used, substantially ( ada does not offer a fast bit-count-on-word operation )

asciilifeform: diana_coman: btw you may find it entertaining that i found several vers of the carry & borrow eqns in my orig notes -- including yours. but for some reason i originally rejected that variant because it needed 2 accesses to the result D . but i neglected to write down why, possibly was simple brain fluke.

asciilifeform: on other front, phf : on occasion of the most recent bolix thread , i went and looked again at the http://btcbase.org/log/2018-01-17#1771955 artifact ; it is interesting that they provided 128 iron types, incl. bignum, but not a 'bignum of fixed N words'. i guess in '80s ~nobody was thinking of crypto at all. ( and i was prolly unduly pessimistic to the orig finder of $item, it is prolly 95% of what's needed for cycle-accurate clone. ☝︎☟︎