asciilifeform: briefly thought 'hey they cloned altera, the specs must now be on the net somewhere'. turns out -- apparently no.
asciilifeform: either way, it helps us not a whit, these items dun seem to be any moar obtainable than 'elbrus'.
asciilifeform: now it is ~possible~ that the spec is disinfo, and in basement of kgb there is a rewritten alteratronic chain. but imho unlikely.
asciilifeform: ( and there is no way to verify that the chip was actually reversed, and produced in ru -- other than to present the specs, and a native clean toolchain ! but catalogue says 'use quartus from altera' )
asciilifeform: the orc packaging ain't a problem, imho it is The Right Thing to ban western smt spec
phf: i suspect there's still some amount of conformance with GOST. i personally think it could be a good practice if done right, but reading some usg account of it i can see how it can be turned into bureaucratic money maker
asciilifeform: ( in modern ru mil production chain, they still mandate ancient orcish pinouts and case dimensions, supposedly to prevent substitution with cheap imported chip with name sanded off )
asciilifeform begins to suspect that these folx simply got a hold of american raw dies and make a killing mounting them in sov-era specced ceramic cases with gold pins, and calling it 'new production'
asciilifeform: 'для проектирования используется САПР ф.Altera − MAX+PLUS II или Quartus II' << pfff yea suggests brute force 'crystal, complete with 'when you care enough to steal the very best' easter egg banner' copy.
asciilifeform: the crud builds up, and you get x86-64.
asciilifeform: suggests that d00dz have the spec ! somewhere.
phf: i should clarify that rather architecture can be improved ~upon~ incrementaly
asciilifeform: in other, slightly related lulz, http://www.vzpp-s.ru/production/catalog.pdf << ru clones of fairly recent altera fpga !!
phf: sure, but chinual is extremely detailed and the ~architecture~ can be improved incrementaly. for example brad's cpu is, yes, implemented as an emulator for a discrete circuit. but at the same time it can be isolated from the bus, put into a determenistic harness, and rewritten from the cpu spec in chinual.
asciilifeform: there's NO reason to emulate, e.g., amd am2900, for all time.
asciilifeform: cadr sucks because it was designed around off the shelf alu and misc glue of the time.
asciilifeform: closing the ouroborus.
asciilifeform: phf: the notion is to build a box with sufficient ram, horse, capacity to drive xterm, so that you can sit down on it and edit the fpga config per se.
phf: i still stand by this point, but with a disclaimer. i think that one of the advantages early hackers had was that they were working from inside their systems. linus was dogfooding linux, symbolics were using every lisp machine at their disposal to build better lisp machines. i think there's inherent folly in planning a revolution from the comfort of our bourgeois machines :p
asciilifeform: no magic 'available until we reversed it, then magically evaporates from market' chips.
spyked: asciilifeform, yeah, it's right below phf's initial reply. the whole thing
asciilifeform: spyked: didja miss the part where it runs on no modern nic ? or the thread where ALL modern nics are built to use dma, which gives the nic vendor access to every byte of your ram ?
asciilifeform: are the hard part.
asciilifeform: reliable controller for usefully large ram, and peripherals ( the only strictly necessary periphs are nic and a reasonable ssd persistent storage )
asciilifeform: spyked: designing a reasonably sane ( a la 'scheme79' ) cpu is not actually the hard part.
phf: now i didn't find out about race conditions myself, that data point came from dks, they discovered race conditions as part of the emulator rewrite, but they have the benefit of having access to the necessary low level bits
asciilifeform: and other nontagged cpu.
phf: i spent (mostly another whisperer and myself did) on getting vlm stable, and i'm unconvinced that some of the issues we encountered were purely "buggy vlm". there is, for example, a crash in floating point instruction that happens when you load document examiner on stock piratebay opengenera. i have no explanation for it still, because vlm code ~seems to do the right thing~. there are other similar instances
phf: http://btcbase.org/log/2017-08-21#1701443 << another little known fact, there are race conditions in genera itself, that manifest in higher clock environments.
asciilifeform: see also the sad story of movitz
a111: Logged on 2016-10-04 15:36 asciilifeform: ACHTUNG, PANZERS! pc engines 'apu2' (the board with the intel nics - vs. 'apu1', with realtek) , turns out, is crippled, hdt probe barfs with it, the cpu is reputed to have a drm fuse set.
asciilifeform: spyked: as for 'use off the shelf iron', see thread http://btcbase.org/log/2016-10-04#1552690 and elsewhere.
a111: Logged on 2017-08-04 22:58 asciilifeform: possibly one could try building a netbsd that doesn't try to touch the usb chip at all. then enjoy setting up sans keyboard.
a111: Logged on 2017-08-04 20:55 asciilifeform: in other noose, asciilifeform took the chance made by the death of ssd in 'zoolag' to attempt netbsd. result : no boot. ( with or without 'no acpi' ) option, hangs at usb init.
asciilifeform: spyked: consider, the amount of arbitrary stupidity you import even ~by having pci bus~ is gargantuan
spyked: asciilifeform, I see. I thought this would be a way to make the problem easier in the short/medium term. but I've had to deal with being at the mercy of X myself at another level so this makes sense.
valentinbuza: hi spyked. I just read the MP blog a week ago :) saw your old comments
asciilifeform: and not a single flipflop of state that we didn't consciously put there.
asciilifeform: spyked: i tried this, it's a dead end because papers over idiot hardware rather than replaces. and does not yield hardware sovereignty-- you are at the mercy of the chipmaker's continued making of 100% compatible cpu & peripherals
asciilifeform: spyked: you will find that none of the existing literature is of any help
spyked: was trying to get a perspective on things. I haven't dabbled in hardware since 3rd uni year (that was almost 8 years ago). and even then... well, I got a lot to learn.
asciilifeform: after this, comes ethernet
asciilifeform: the other aspect, vlm is a massive bucket of c liquishit, and not at all a compact description of the arch
spyked: ok, so to sum up; 1. get ice40 fpga; 2. run fpga lisp machine (cadr?); work from that towards symbolics/ivory, or the other way around starting from symbolics.
spyked: although I'm expecting the code to have its own hacks
spyked: asciilifeform, yeha agreed. was wondering whether it's worth using the virtual machine as a starting point.
a111: Logged on 2017-08-21 11:33 spyked: also, is there any worth in trying to "physicalize" the virtual lisp machine stuff? genera runs on that from what I read.
asciilifeform: http://btcbase.org/log/2017-08-21#1701413 << to get the fuck off unix and pc. permanently.
spyked: phf, slither.io is very similar to agar.io, which was similarly addictive back in the day. killed a lot of hours with it, so from that perspective, definitely wouldn't recommend trying it
jhvh1: spyked: The operation succeeded.
a111: Logged on 2017-08-20 01:23 mircea_popescu: !~later tell spyked http://thetarpit.org/posts/y03/062-greenspan-assault-on-integrity.html << the problem with this view is that the pantsuits correctly intuit that all the imbeciles they enfranchised are sitll imbeciles. consequently it would be no harm to a business' reputation to sell them iguanas on a stick and call it prime beef. they will never know ; and casual perusal of tardstalk "investor" as well as "community disc
spyked: !~later tell mircea_popescu re http://btcbase.org/log/2017-08-20#1701196 <-- yah, but does protecting the "proles" from own stupidity even make any sense as a statement? sorta relates to idea on Trilema on whether the empire wanted to arrive to this point (can't find it right now). enfranchisement of the stupid directly lead to that.
spyked: also, is there any worth in trying to "physicalize" the virtual lisp machine stuff? genera runs on that from what I read.
a111: Logged on 2017-08-19 23:57 phf: fwiw, if the goal is to put an existing lisp machine onto an fpga, then i don't think macivory is a particularly good target. the goal would be to run Genera, which is severely lacking sources for critical components.
spyked: phf, asciilifeform: re http://btcbase.org/log/2017-08-19#1701146 http://btcbase.org/log/2017-08-20#1701180 <-- thanks for all the refs. my initial plan was to start from whatever SECD papers I could find and better understand architecture specifics.
mircea_popescu: and in other "us entrepreneurship" aka "the incredible productive assets and unlimited human ingenuity existing in America?", i give you https://www.youtube.com/watch?v=fyw3lZ8Jw7E
mircea_popescu: griffith is against. matthau comments importantly that "at least he has the courage of his ignorance".
mircea_popescu: BingoBoingo amusingly, the "welfare state" / entitlement program is actually discussed in the film!
BingoBoingo: http://trilema.com/2017/a-face-in-the-crowd/#comment-122723 http://nation.foxnews.com/?q=health-care/2010/09/08/obamacare-destroys-andy-griffiths-approval-rating
BingoBoingo: http://trilema.com/2017/the-story-of-friday/ << Remember
BingoBoingo: Holes collapse on themselves
BingoBoingo: They can't even bend their own to follow the groupthink when targeted for the minute of hate
mircea_popescu: i thought that was the whole slippery point of zher, that there's a hole not a line.
mircea_popescu: phf also worth bearing in mind that point re introductions in the rothbard series. people more recent than the author daring to pen introductions are the exact equivalents of herostratus ; and to be treated no better.
mircea_popescu: there was one major cultural power in the time uncultivated minds can furthest think back to, a time whose murmurs come to them through the great-grandparents, and that time wasn't napoleon 3's paris. it was vienna.
mircea_popescu: for the record, most of what orcs (ie, americans, russians, etc) think when they imagine "Great Ole European CULTURE!!" is actually exactly between moscow and berlin : 100% spritz and http://btcbase.org/log/2015-07-09#1195397
phf: in other words i'm slowly discovering that there's life west of moscow, but before you hit berlin :o
phf: and the introductions to eliade's book don't go into apologism (unlike evola books, all the english translations require an mandatory disclaimer, that he was a racist, but only a little!1)
phf: well, tbh i only just learned that the two knew each other. evola is mentioned in eliade's books, but only in connection to his books on subj, like "the yoga of power" and his study of pali canon
mircea_popescu: phf fwiw, culianu was actually killed by the national-socialist PCR (romanian communist party).
mircea_popescu: http://btcbase.org/log/2017-08-21#1701362 << this probably captures the "stealing by name" pantsuit doctrine best.
mircea_popescu: http://btcbase.org/log/2017-08-21#1701361 << hey, it's not like herdemocracy happens on accident. insistently, persistently built why whole swathes of shitheads.
a111: Logged on 2017-08-20 23:50 phf: one, Ioan Culianu, who was in turn killed in 91, some say over his criticism of romanian right, but of course we all know that he was dispatched by the occult interests over his research in that field.
phf: http://btcbase.org/log/2017-08-20#1701331 << for the curious http://linguafranca.mirror.theinfo.org/9209/culianu.html
a111: Logged on 2017-08-21 03:05 phf: fare: "I'm all for supporting old implementations (we support Genera, furgossake), but that's very different from supporting an old ASDF. ASDF was designed to be self-upgradable precisely so that the way to deal with an old ASDF is to upgrade it."
phf: from "Change some defaults to more reasonable values" attila-lendvai "the key bindings in the connection list are currently very dangerous when using with production systems, e.g. killing the connected lisp is bound to a mere C-k."
phf: fare: "I'm all for supporting old implementations (we support Genera, furgossake), but that's very different from supporting an old ASDF. ASDF was designed to be self-upgradable precisely so that the way to deal with an old ASDF is to upgrade it."
phf: i went reading slime/swank pull request conversations on github (i know my mistake!) and it's all the usual wreckers there.
Birdman: ah yeah, did i request that, i dont know why i would lol, its the winners of the hands i need to de clutter
mike_c: it lists the missing player(s)
Birdman: right now it lists the players that left right?
jhvh1: mike_c: The operation succeeded.
mike_c: Uh, sure, that's easy. Just for the bad hands you mean?
Birdman: but this is still really helpful helpful, so no luck on listing the hand winners ?
Birdman: yeah for some reason i think it lists the blind number instead of just what the blind is. that must have been the one million and change blind posted
mike_c: asciilifeform - closed turd client was necessary because I didn't think this would even work, and it was one time thing. so not worth investing time in vs. spinning up VM and then destroying it.
mike_c: But that should get you the hands you are interested in.
mike_c: I can't actually fix the numbers for you, because the numbers are wrong. Note in the example how it says the small blind was 1 million and change.
mike_c: This only identifies hands where someone put money in the pot and wasn't in the summary. Cuts it down to 1,591 bad hands out of the 300k
jhvh1: mike_c: The operation succeeded.
phf: one, Ioan Culianu, who was in turn killed in 91, some say over his criticism of romanian right, but of course we all know that he was dispatched by the occult interests over his research in that field.
phf: little known fact, mircea eliade was at some point a member of iron guard, and later tried to repent, mostly to preserve his academic legitimacy. still some accuse him of peddling evolan party line under the guise of legitimate scholarship. he was ousted by his own student
mircea_popescu: it';s the exact same thing.
mircea_popescu: it can't be the opposite. not on amazon, not with the stupid title, not with that schmuck from "culture wars" magazine hurr durr.
r0nin-: well i believe the content is available off amazon too
mircea_popescu: no. it is actually trying to bill itself as the opposite.
r0nin-: its actually the opposite
mircea_popescu: the odds of my reading amazon offerings of ustardian pantsuit nonsense are nil.
mircea_popescu: r0nin- sure, about 50% of the girls "think he's great" pre-enslavement.
mircea_popescu: http://trilema.com/wp-content/uploads/2013/05/noua-carticica.pdf << end produict, for the curious.
mircea_popescu: that's the extent of familiarity, i had to review the god-awful prose of the interwar imbeciles as part of writing the programme.
mircea_popescu: ah. i tried to (intellectually, and financially) sponsor the "romanian new right". they weren'tr capable of digestion.
BingoBoingo: Well, She isn't actually. She's part of the environmental hazard
asciilifeform: in the land of pubs with 400 car lots
mircea_popescu: i don't get it, her solution is to not leave the house ?
mircea_popescu: and in other heart shapes, http://68.media.tumblr.com/ca75e1bdb7d88cc7cc2d285eee7634d6/tumblr_nbwg21kIVh1s9gtmoo1_1280.jpg
valentinbuza: While other universities (Math Unibuc) had some.
valentinbuza: as you can see https://ocw.cs.pub.ro/courses/ic/start, the material is the same as "advanced" course
valentinbuza: I have some clarification about choudary dude. He is a recent professor (1 year) at our university. The course is called "advanced" because from this year onwards will be advanced material.
jhvh1: phf: The operation succeeded.
phf: !~later tell spyked damn you, i spent an entire night playing slither.io
asciilifeform: meanwhile, in the world of traitorously redacted wickylicks, https://archive.is/Zus30
mircea_popescu: this is like 9 yo telling you that the bath dissolved her snatch. you can't corrode just the seam, as a concept, leaving behind the item without a seam can oyu.
asciilifeform: ( but is it possible that the seam vanished from corrosion, with rest of surface? in ancient pot )
mircea_popescu: the greek items can grow larger, and offer no visible seam, and so on.
asciilifeform: ...the item one boils in oil in?
mircea_popescu: but ifg you look at the 1k pre-bc greek cauldrons, the similarity to 1500 ad english castle pots is striking. just... the metal is about 100x finer in the ancient case.
mircea_popescu: neither a very convenient proposition.
mircea_popescu: anyway, funny thing re bronze : it needs tin. as far as ancient world is concerned, copper was uberabundant (cyprus) but tin was either england or anatolia
mircea_popescu: asciilifeform they had cannons, just didn't use them as cannons because no gunpowder.
mircea_popescu: in point of fact there was NO item more advanced in 1700 england trhan there was available in 200bc athens.
mircea_popescu: asciilifeform could have refined it once started, much like the english did.
mircea_popescu: for same applications as historically -- mining first, then crop/textile processing, then boat power.
asciilifeform: well if you dun care what kind of movement - they had it
asciilifeform: ( leaving aside the notion of bronze pressure vessel )
asciilifeform: need lathe for symmetrical parts.
mircea_popescu: they DID make some bronzeamphorae. but had no idea what to do with it.
mircea_popescu: consider, they made bronze statues. and had very advanced pottery.
mircea_popescu: but the greeks had the metallurgy to introduce the early steam engine, just like the english did.
mircea_popescu: maybe, though really, it was cost effective in 200bc. they were just dumb.
mircea_popescu: the problem with these "breakthroughs" and "genius inventions" in the industrial setting is that they're generally ancient lore finally dug from under the mound of economical impracticability.
mircea_popescu: not new, either. only became cost effective recently, but otherwise this is 1960s tech
mircea_popescu: anyway. the idea of forced ion exchange so the surface gets potassium-doped and thus micro-tensed and somewhat stronger is not bad.
asciilifeform was just drinking from these
jhvh1: mircea_popescu: The operation succeeded.
mircea_popescu: !~later tell spyked corning gorilla glass is just alumino-silicate glass made by corning. there's a bunch others. think of it as cheap bohemian glass, that thing we had the 10kg fruit bowls etc, "cristal". that's leaded, this is aluminized.
mircea_popescu: there is ~no possibility~ of such a tging as reputation among africans, shamanists, idiots, "what good are square roots" and other sub-human non-people.
mircea_popescu: !~later tell spyked http://thetarpit.org/posts/y03/062-greenspan-assault-on-integrity.html << the problem with this view is that the pantsuits correctly intuit that all the imbeciles they enfranchised are sitll imbeciles. consequently it would be no harm to a business' reputation to sell them iguanas on a stick and call it prime beef. they will never know ; and casual perusal of tardstalk "investor" as well as "community disc
mircea_popescu: and in other couples, http://68.media.tumblr.com/07e78476529bf98675c72ebdc456a5df/tumblr_nbsagh1pwo1s5gthao1_1280.jpg
phf: well, it's the prototypical "mud ball"
asciilifeform: the sad part is , apart from the ONE basic win ( tagged word memory ) the lm arch was ~= that kalash, 'shit bolted to all sides'
asciilifeform: ideally would end with the 'good parts' -- the genera envir -- without the rubbish ( the byzantine hacks around specific amd alu chip quirks, the multitude of special purpose busses, the constricted addrspace )
phf: but i agree on the overall points, though moving forward from cadr wouldn't be so much backporting, as "writing in the missing bits"
asciilifeform: the pc emu quasi-worked
asciilifeform: phf: i haven't tried the fpga one
asciilifeform: i.e. baked around various arithm chips available at the time, rather than raw transistor
asciilifeform: best of all, of course, would be for somebody to leak / steal the missing bits.
asciilifeform: phf: i'd rather spend next decade reversing the bolix firmware, than wintel liquishit
phf: there are extant lisp machines that have both hardware documentation and system sources, for example MIT's CADR, but cadr specifically predates symbolics by a dozen of years, was developed by academia, so it's nowhere near as advanced as genera
phf: in a sense that it's a massive code base that works, but if you want to have full ownership, you'll have to fill the source-less bits yourself
phf: i'm actually not even sure how much code is there, but what's critically missing is the low level bits that talk to hardware
phf: yeah, i fat fingured enter before making the entire point
phf: but it doesn't have all the source code.
mircea_popescu: so genera-ivory then
mircea_popescu: so you want to implement the software in fpga ?
phf: genera is the software layer to ivory's hardware, it's usually what people are talking about when "superior development environment!11" etc. symbolics architecture is crufty idiosyncratic, so taking its hardware without also the software doesn't make sense
mircea_popescu: and in other tight couplings, http://68.media.tumblr.com/1d311e42a24764b32eb521e60adcfd62/tumblr_nt9ft5KbHE1tcl9sho1_500.gif
phf: fwiw, if the goal is to put an existing lisp machine onto an fpga, then i don't think macivory is a particularly good target. the goal would be to run Genera, which is severely lacking sources for critical components.
a111: Logged on 2017-08-19 19:29 spyked: asciilifeform, found something (in romanian) http://www.atic.org.ro/ktml2/files/uploads/Masina%20DIALISP.pdf there's also a more detailed english version on ACM sci-hub http://dl.acm.org.sci-hub.cc/citation.cfm?id=802028#
BingoBoingo: Shame this poor mother can't send the author back for a warranty claim. https://archive.is/phQzk
jhvh1: BingoBoingo: The operation succeeded.
BingoBoingo: <mircea_popescu> BingoBoingo so what's the story, is flake making it in az ? << My lulz scroted crystal ball is hazy at the moment
spyked: asciilifeform, found something (in romanian) http://www.atic.org.ro/ktml2/files/uploads/Masina%20DIALISP.pdf there's also a more detailed english version on ACM sci-hub http://dl.acm.org.sci-hub.cc/citation.cfm?id=802028#
asciilifeform: it was a diesel-electric. was taken as spoils by su, and briefly was the only source of mains current in odessa when asciilifeform's father moved there as a boy
mircea_popescu: generation of kids who all loved legos and their world is more fragmented in stupider ways than the 1600s mercantilist world. wtf.
mircea_popescu: the correct move is towards a |ing of hardware, and of software, and everything else.
mircea_popescu: cli works fine because of the | and so on.
mircea_popescu: anyway. the point being that competition should happen on narrower elements.
spyked: yeah, but must still be of some use though. I don't know if there's even a genuine Lisp machine in ro
mircea_popescu: they're the ~copies~ of minoan vases produced in syria, not the actual minoan vases.
mircea_popescu: this is artisanship, after a fashion, but not to be confused with the genuine article imo.
mircea_popescu: spyked see, the thing with orc lands is that they have this. borz, chechen made smg. the egyptians made engine parts to VISUAL spec, by hand. i saw this. guy here offered to produce a replacement pressure hose for me, by visual inspection.
spyked: asciilifeform, I'll ask around, see if I can dig stuff out of the archives (assuming there are archives)
mircea_popescu: well then.
diana_coman: mircea_popescu> romania's computer independence program huh. <- most of the old profs at UPB that I still got to know had worked on some parts of that from what I gathered
mircea_popescu: spyked was it a cartpenter you hired, ie, a guy who worked in wood, or was it an ikea clonal system you hired, ie a guy who went to a central warehouse where they cut some glue-dust planks to his spec ?
asciilifeform: spyked: i'd be curious to see the ro lm
mircea_popescu: i assemble my computer out of parts to no great sufferance, and get for my trouble a much better computer than any of the pre-made buying dorks.
mircea_popescu: spyked consider that most consumer products come kitted anyway, and when you buy a car your question is "well is the engine from mexico or brazil or germany ? is this the original transmission ?" etc.
spyked: mircea_popescu, I agree. do you mean"the fridge" as in somewhat close to the platonic fridge?
spyked: diana_coman, but giumale retired. btw, I know he made a Lisp machine clone back in the 80s. the hardware might be lying around somewhere in the faculty.
mircea_popescu: software is the worst offender here, but hardware is also pretty bad. consider -- i don't want to buy "A fridge", i should buy standardized compressor units, and so on. why do i want "the fridge" ? there's no need to debate "whirlpool" vs "obamacare". compare discrete items.
mircea_popescu: re http://thetarpit.org/posts/y03/04e-the-myth-of-software-engineering-iii.html << hjere's the thing, let's posit that an object larger than what fits in head can not exist. this may seem counterintuitive, but it happens to also be correct. now, the direct solution to the problems of "exponential dependencies" and "clarity of purpose" and so on is that these have to be defined by domain boundaries. once you have this implemen
diana_coman: o.O ; there used to be giumale's programare functionala - quite an eye opener that course
mircea_popescu: eh, the paradigm gotta shift from this pasty ass "ima try and make a lot of moneyz so maybe im left with something after wife dolchstoss)
spyked: I resisted many attempts to turn the "programming paradigms" (Lisp/Haskell/Prolog) course into a Java thing.
spyked: anyway, the one and only advantage of UPB CS department is that for now it still has the resources to bring up smart people, most of which unfortunately turn into goog/fb/whatever employees. I don't think that's gonna last for long though. wish it did, but...
mircea_popescu: whereas romanian "right" at least in the sense of, parliamentarily, is very much washington democrats, all into eu bureaucracy and occasionally inadequate liberal economic policies.
mircea_popescu: they're historically pro-russia and pro-independence, grudgingly pro-eu cuz "da people". but otherwise populist and strong in the equiv of us red areas.
mircea_popescu: asciilifeform ro social-democrats are rather a sort of "central republicans".
asciilifeform: vs what other academics?
spyked: sure thing. I can reference the Trilema posts on crypto
spyked: he's okay, we chatted a few times, but I don't know him very well. it's hard to judge most people in the faculty higher than by "mint rubber or not", and he's pretty hard working at least.
mircea_popescu: perhaps it was god-given ? came out of the pantsuited hilarity's hairy snatch ? who knows.
asciilifeform: gotta love how the 'side channel analysis' people ~to this day~ have not produced a fixed-time rsa.
spyked: mircea_popescu, yes, he's an assistant prof. in the cs department. works on crypto and some hardware stuff (side channel analysis)
mircea_popescu: this is nice, especially when found magic weapon in the field. but also very useless.
mircea_popescu: the problem with getting "engineers" to construct proofs in this vein is that engineers have too much monkey in them. "doctor, doctor, if i shove it in this way it works!"
spyked: the whole thing is. and yes, this is "formal verification 101" taught in universities. if you want to get even more outraged about it, read Heiser's post at the beginning.
mircea_popescu: it ends up as being an example as to why it is hard to think about systems if one's very inclined to unhygienically import random unknowns into the workbench.
mircea_popescu: "We may informally state that "reversing a given list yields the list which has the same elements but in the exact opposite order (e.g. right-to-left, as opposed to left-to-right)", but we have no way of accurately specifying this in our language other than by defining rev and postulating that "rev reverses any given list". The same goes for appending lists."
spyked: yeah, it was very easy to conflate "list can be described as either nil, or pair between something and a list" and "list is defined as". I could rewrite sometime if you think it's worth it; I don't think it is, I was just trying to show how reasoning about software isn't trivial even when you have a framework for that, let alone when void *p = ...;
mircea_popescu: spyked no, see, you already reference "arbitrary order" without having even discussed the matter. why is a list ordered ? how is it ordered ? can penis pushe ice cubes not be a set ?
mircea_popescu: but in my experience, generally people take refuge in minutia when scared of biting the problem. wtf difference does it make how i construct an enumerated set, maybe i push icecubes off the table into the paper bin with my penis.
mircea_popescu: im not sure there's any way whatsoever.
spyked: hm. you mean, there's a long way from "enumerated set" to 1:2:[] which I skipped?
mircea_popescu: it's a set, and enumerated because computers lack the ability to construct ~described~ sets, such as "the set of prime numbers" or w/e.
mircea_popescu: you're equivocating between definition and constructor! wtf is "a list is... : is the list making operator so a list is 1:2:[]" nonsense!
spyked: mircea_popescu, no. I know Inria guys made a verified compiler. with the caveat of "abstract nonsense". anyway, tmsr search yields stuff :)
mircea_popescu: re http://thetarpit.org/posts/y03/057-reversing-lists.html you know the story of thomson's compilers yes ?
mircea_popescu: there's that.
spyked: true, but it seemed like a good idea at the time. and I can do it incrementally (the current blog works. it lacks comments, that may piss people off, but it's not like I get too many readers)
mircea_popescu: yes, but prioritits. there's larger fires burning.
spyked: mircea_popescu, no. lol. nobody's working in the uni during this time of year. I'm expecting it to come back up... in September maybe
spyked: I'm guessing a lot of people here use Lisp for their implementations. :) I got into it after first reading asciilifeform's laws of sane computing
mircea_popescu: spyked the thing you used to search btw, runs in lisp.
spyked: my initial thought on getting a Lisp machine run was using a RISC machine as microcode. and implement the whole thing bare metal in software. it's a lot cheaper, albeit probably hard to verify
mircea_popescu: turns out the whole hello & welcome works out a lot better when i don't have to ask "so who are you". who could have predictated.
spyked: hm. this is neat stuff. I know opencores had some free Lisp FPGA designs. never tried any of them though.
mircea_popescu: in theory it could be fit on a fpga.
mircea_popescu: http://btcbase.org/log-search?q=ivory << better search than google. anyway, ancient tech, symbolics co. lisp machines from teh 80s. there's (some, limited) effort to cut up the chips / redo the whole thing.
mircea_popescu: either/or. but generally throwing out and redoing comes up a lot
spyked: oh. so reverse engineering the blobs and/or reimplementing? that's actually pretty neat