log☇︎
59100+ entries in 0.033s
asciilifeform: the procedure for making the 'road' go is quite elaborate and much dwelled on in ru prison lit. ( gotta pull apart a sock, weave rope, make 'fishing rod' out of paper + bread glue etc , then run the 'horse' )
BingoBoingo: Anyways, Libertad is about a third of the way from Montevideo to Colonia
asciilifeform: d00d whose cot is by the grate has the duty of 'keeping the road', as they called it (again nfi in english world what it is called there, much less in spanish empire)
asciilifeform: look specifically in http://archive.is/M4NEr -- the center 2 cells on bottom 2 rows are linked with horses
BingoBoingo: I am unsure, I missed them in the photo until you mentioned them
asciilifeform: one hooks up wads of paper with note , like spitball in kindergarten, to'em
asciilifeform: ( in ru world they're кони , 'horses' )
asciilifeform: y'know, between the adjacent cell grates
asciilifeform: hey BingoBoingo what do you call in english those strings ?
Mocky: is it just me or does that look like baltimore?
a111: Logged on 2017-08-22 18:12 mircea_popescu: this place is for reading AND FOR CHANGING YOURSELF.
a111: Logged on 2018-11-30 09:12 mircea_popescu: asciilifeform right, "lalala i can't hear you" until the very last moment, when the curtain drops. because why the fuck not, hurr.
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: https://github.com/project-everest/hacl-star/blob/master/code/bignum/Hacl.Spec.Bignum.Fproduct.fst << holy fuq, the sort of liquishit that d00d's links offered as proofolade... picture trying to ~read~ this. ( and there's 9000 of'em )
mircea_popescu: all this "self-confidence is the only education needed" nonsense reheheheally paid off.
mircea_popescu: asciilifeform right, "lalala i can't hear you" until the very last moment, when the curtain drops. because why the fuck not, hurr. ☟︎
zx2c4: My "nice post" remark wasnt sarcastic, if thats what youre responding to
zx2c4: On my phone right now, woke up from a dream to see this, not sure if im still dreaming. Care to explain what's provoked your ire?
mircea_popescu: next shit out of your dumb mouth fails to string match apologizing for being quite so fucking stupid, i'ma fix the negligence whereby you can still speak here. ☟︎
mircea_popescu: what the everloving fuck.
mircea_popescu: http://btcbase.org/log/2018-11-30#1876164 << dude, get the fuck off the planet, and take your pompously vacuous self-important idiocy with you. ☝︎
asciilifeform: btw , q for ffa readership, can anybody think of a way to make the digit slider routine non8bitbyte-clean ? ( beyond having ffa eat its pistol on boot if it finds itself on such machine, lol )
asciilifeform: i'ma bet was not acctd for in the 'proof'isms..
asciilifeform: ( longtime tuned-in folx, will know what irons )
a111: Logged on 2018-11-30 03:22 asciilifeform: ... or that the #define ULT(a, b) ((a ^ ((a ^ b) | ((a - b) ^ b))) >> (sizeof(a) * 8 - 1)) macro dun turn to barf in the preprocessor on acct of some esoteric beard shaving from dennis richie ?
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: http://btcbase.org/log/2018-11-30#1876333 << dun seem to be in the logs, possibly was in a private letter from sumbody.. ☝︎
asciilifeform: it's sitting in a 3ring here in my tortureroom for whatever reason.
asciilifeform: iirc you recced it last time
zx2c4: ever see this book https://jjj.de/fxt/fxtbook.pdf
zx2c4: aahh that trick
zx2c4: or, rather, where can i see the implementation of W_Carry
asciilifeform: it is result of the specific mathematical approach taken. where code must remain SMALL and NO branching on cryptobits, other than death on div0, is permitted. no memory indexing on cryptobits, either.
asciilifeform: tho it does helpfully give pascal-style pass by ref, to avoid pointerisms
zx2c4: what you've described sounds good. im wondering if it's the result of comments, the result of just better organized code, or the result of some nice features of ada you're using
asciilifeform: consider to read the series.
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.
zx2c4: dennis probably wants those variables surrounded by ( )
zx2c4: "unsigned less than"
asciilifeform: ... or that the #define ULT(a, b) ((a ^ ((a ^ b) | ((a - b) ^ b))) >> (sizeof(a) * 8 - 1)) macro dun turn to barf in the preprocessor on acct of some esoteric beard shaving from dennis richie ? ☟︎
zx2c4: right. shows that the carrys work out without overflows given certain bounds on the input
asciilifeform: does your proof demonstrate that none of them can overflow, regardless of what happens , say ?
asciilifeform: what i see in the link, is a buncha c code, with pointerisms
asciilifeform: lessee the proof ?
asciilifeform: can you, for the one for that routine you linked ?
zx2c4: in the example above, its pretty easy to prove that by hand
asciilifeform: if you can follow the proof by hand
asciilifeform: it dun verify jack shit. is machine barf. just like the raw output of your compiler, except less meaningful
zx2c4: in addition to reasoning about it
zx2c4: later if im changing the code
zx2c4: i save my z3 script so that
asciilifeform: whereas 'here is my z3 proof' is typically published for cachet among haskellist co-religionists
zx2c4: rather than proof
zx2c4: i think in crypto most people refer to it as "verification"
asciilifeform: then why do you advertise and publish the 'proofs' ?
zx2c4: and then think backwards in order to reason about its correctness later
zx2c4: it also lets me try things super fast without thinking
zx2c4: oh. yea, as i said, they're mostly just tools
asciilifeform: to jump on ~your~ parachute, that you sewed.
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.
zx2c4: no. they're mostly just tools
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: zx2c4: lemme ask you this -- those mecha-proofs of yours, how much do you actually believe in'em ?
zx2c4: that z3 script gives a little more assurance we didn't screw up the radix conversion here
zx2c4: z3 is nice for things like
asciilifeform: sucked beyond my ability to describe.
zx2c4: (i learned algebra back in the day from a professor who wrote a haskell program to generate our textbook... presumably in your mind, my foundational education could not be more screwed up https://en.wikipedia.org/wiki/Dave_Bayer )
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: homeopaths at least only bamboozle the irredeemably stupid
zx2c4: more seriously, if you're mostly after small computer programs to help you out when exploring a field but eventually do the proof by hand, z3 and sage wind up being super practical as day to day work horses
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 ?
zx2c4: well, as it turns out, coq had some amazing fallacy in its core code a few years back resulting in the ability to prove any statement true...
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 )
zx2c4: i can see that critique of haskellism. endless intellectual masturbation (hello trilema?) that doesn't actually drive at any essential truth. there's a particular benefit in demanding truths remain small rather than large
asciilifeform: zx2c4: lemme ask, on what authority am i to accept the correctness of a proof generated via e.g. coq ?
zx2c4: (coq is from the late 80s. its still in use, but i guess you could use the 2009 version...)
zx2c4: I agree with you in spirit -- I think learning details of a proof enough that you have all of it in your head is a good pedagogical approach and gives you more mathematical agility as you progress forward. I just don't know about the ontological statement regarding the proof's validity
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
zx2c4: hey i like good ol rs232 too
asciilifeform: or that ~ nuffing in asciilifeform's machine room postdates '09
asciilifeform: or that FUCKGOATS rng is built to speak rs232 at 115200 baud and always will be
asciilifeform: ( wait till he learns that asciilifeform has a fleet of e.g. dos boxes. )
zx2c4: oh. then derive and macsyma surely are jokes
zx2c4: a temporary buffer, rather than a rolling log
zx2c4: so perhaps you prefer chalk and slate to paper then
asciilifeform: but they are devices for eventually rearranging contents of your head, permanently, rather than substitutes for head,
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'
zx2c4: alright and you'd freely admit that when you write things down and solve intermediate lemmas, its often the case that by the time you get to the end, you don't have in the forefront of your brain the details of all intermediate steps anymore
asciilifeform: so long as in the end it clicks in your crankcase and is as obvious as that and gate.
zx2c4: so this state of "being proven" for you -- it requires some kind of intuitive bullet shot from start to finish of all particulars of a certain logical progression? and any deference of that to outside tools (like paper, or intermediate results with forgotten details) ruin the intuition?
asciilifeform: let's take from other end of digestive tract. consider 1 AND gate. idealized, no metastability, no breakdown voltages, literally 'ands' two logical values. ( can have physically limited to % of c speed, if you like, but this is uninportant )
zx2c4: > At this time we will walk through the mechanics of our Karatsuba multiplier, so as to cement in the reader’s head the correctness of the routine, and lay groundwork for the optimization which is introduced in Ch. 12B.
asciilifeform: the attribute which permits this approach, vs haskellism and other idolatrous rituals to mechanical molloch, is called 'fits in head'.
zx2c4: I more or less know the process involved but don't have all of the steps in my head. And as I wrote it down, I forget the details of previously written steps while working out current new steps. Yet I have faith in the process of writing it down systematically and having intermediate results from pages prior
asciilifeform: ffa. see esp the passage re parachute.
asciilifeform: fortunately there is a convenient demo
zx2c4: There are some things I could only prove if I had a paper
asciilifeform: gotta actually exist ( and 'genius' btw is the fella who makes the 'fit in 1 head' fit in 9000. )