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.
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 ?
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: sucked beyond my ability to describe.
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
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: i sometimes even use computer algebratrons, in exploratory work. but would never consider presenting output straight from one as 'here, correct'
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'
asciilifeform: so long as in the end it clicks in your crankcase and is as obvious as that and gate.
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 )
asciilifeform: the attribute which permits this approach, vs haskellism and other idolatrous rituals to mechanical molloch, is called 'fits in head'.
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: ffa. see esp the passage re parachute.
asciilifeform: fortunately there is a convenient demo
asciilifeform: this is a political declaration, not an astronomical observation, zx2c4
asciilifeform: zx2c4: theorem that dun fit in any 1 skullcase, aint proven.
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: proof is proof when it fits in head, now just as in euclid's time.
asciilifeform: wtf is the point of 'here's a proof but you need this here 100MB of gnarl to ~run~ it and of course you will trust output, or are you a terrorist'
asciilifeform: and, in parallel, to be an organized campaign of sabotage against ~concept~ of actual correctness in programs.
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: zx2c4: weren't you here last yr for a 'the technical cannot be separated from the political' and 'if program+all accessories doesn't Fit In Head, it is garbage, not proof' thread ?
asciilifeform: mircea_popescu: wx liquishit , qt, jettisoned loong ago. but bdb, openssl , boost, remained
asciilifeform: ( observe -- sans agression, the moar reliable is your hosting, the ~more~ certain your noad is to get perma-wedged, as it'll never reboot and never satisfy shitoshi's 'catch up only on cold boot' idjit condition.. )☟︎
asciilifeform can't even count nao how many time had convo, 'hulp! my noad is hanging' 'didja aggression' 'no...' '...'
asciilifeform: srsly, whoever's poor neglected box this is -- fucking put in 'aggression' or pull the plug, thing is eating mains current to no useful end
asciilifeform: anyffing that dun make immediate sense in ~that~ light oughta be either changed or commented.
asciilifeform: diana_coman: this is a+++ good, it is exactly how it is meant to be read
asciilifeform: my current aim is that in ch22 ( see also http://www.loper-os.org/?p=2735 ) any subcomponents not used, are to be cut; and any that have strictly 1 invocation, are to be made sub-functions and remain visible solely in the scope where used.
asciilifeform: orig was writing from pov of 'most general possible set of subcomponents' , but this is not necessarily what is wanted in the end product, esp. from loc-cut pov.
asciilifeform: (this is, for most part, already what cmdline does. aside from 'maxsteps' not having yet been introduced Officially, cuz no loops yet)
asciilifeform: i.e. one will call, roughly, P(pcodestring, ffawidth, ffaheight, maxsteps) and get output.
asciilifeform: incidentally even the currently given 'external api' is eventually to be 'internalized', in the sense that user input is expected to be in P-code (presently named as 'ffacalc') and output ditto
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: but the same guarantee cannot be given for erry internal component, not without geological runtime.
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: observe that the operators of fz_shifts are not exported in ffa.ads ( ch11 unified api ) , they are strictly for internal use in the lib.
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: you mean, what if one were to feed it one when cascading ?
asciilifeform: diana_coman: how would a shift by 2 provide overflow of 8 ?
