< 1268006404 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :1::2::3::nil is represented as <3, {yes->1;no->2;maybe->3}> < 1268006424 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :r::q::p::::snil is represented as <4, {north->1;south->2;east->3;west->4}> < 1268006427 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :oops < 1268006435 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :r::q::p::s::nil is represented as <4, {north->r;south->q;east->p;west->s}> < 1268006440 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :aha < 1268006443 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :gotcha! < 1268006448 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ok, so what's the induction for T'? < 1268006458 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :why don't you write it < 1268006463 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :ill tell you if you get it right :) < 1268006467 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :look at O for inspiration < 1268006535 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Pr < 1268006547 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Ordinarily I'd love to, but - I really should have left many minutes ago. < 1268006569 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You could save the dialogue for later, I'd love to participate, and just show me the induction schema for mu now for me to mull over. < 1268006577 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Or you could wait for both. Your choice. < 1268006714 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :there is no way you can possibly understand the scheme for Muu < 1268006729 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Likely. < 1268006729 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :You have to first understand T < 1268006735 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But I'm interested in it regardless. < 1268006747 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :it will be very simple and clear once if you just approach it step by step < 1268006785 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Yes, but I /really really/ have to go. Surely, there is no harm in telling me it? < 1268006795 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :well I don't know how to write it out either < 1268006807 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :we need to establish some new notation together first < 1268006825 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :just use any existing language :P < 1268006829 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :or are they not appropriate? < 1268006851 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :P(L') -> (forall n, forall f, (forall i, P(f i)) -> P(B' f)) -> forall t', P(t') < 1268006858 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :that's the scheme for T' I wish you had got it < 1268006883 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i probably would have if i tried < 1268006888 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but /i/ /have/ /to/ /go/ < 1268006891 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :please try and understand < 1268006893 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :bye, anyway < 1268006897 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :so for T, P(L) -> (forall l, [] P l -> P(B l)) -> forall t, P(t) < 1268006908 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :[] is a new notation we have invented < 1268006923 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :[] P (a::b::c::d::nil) = P a /\ P b /\ P c /\ P d < 1268006949 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :[] is defined for any strictly positive functor < 1268006960 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :(proof of this is in some paper I can show you later) < 1268006967 0 :MissPiggy!unknown@unknown.invalid PRIVMSG #esoteric :this is enough to define induction on Mu < 1268007067 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It's the end of days for There. < 1268007137 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :"•DSL/Cable modem: 25 minutes" < 1268007143 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :for a 47MB download < 1268007164 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268007457 0 :FireFly!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268007757 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268008323 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268009298 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wants to play on FICS against someone he knows < 1268010107 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION has been futzing a tiny bit with TinyGC... < 1268010119 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... It appears to work, and appears to be slow. < 1268010120 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yeah. < 1268010162 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: what's your rating? < 1268010183 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :coppro, um, it's been years since I was last on FICS < 1268010185 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :How do I get that? < 1268010192 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: oh, ok < 1268010195 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :then I'll play you < 1268010197 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Found it < 1268010209 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I just didn't want to play against someone way better than me < 1268010211 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Um, rating for Blitz or Standard or Lightning? < 1268010220 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :coppro, I'm probably not better than you < 1268010220 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :don't really care < 1268010225 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :It's been years since I played chess < 1268010383 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: what time controls do you want? < 1268010392 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :*shrug* < 1268010415 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Regular, I guess < 1268010457 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: it says you're examining a game < 1268010462 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What? < 1268010476 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :there we go < 1268010734 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION clearly has no clue what he's doing < 1268010776 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I only have a little more than you < 1268010795 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :I can give you some pointers afterward, if you'd like < 1268010929 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Sure < 1268011026 0 :MissPiggy!unknown@unknown.invalid QUIT :Quit: Lost terminal < 1268011038 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION isn't really thinking anything through that much < 1268011221 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :You went downhill around move 16 < 1268011826 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I've lost, haven't I? < 1268011893 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric ::(:(:( < 1268011953 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :mostly < 1268012061 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :[In case anyone cares, I just lost] < 1268012066 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :coppro, what client do you use? < 1268012074 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :eboard < 1268012085 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :it's not great, but it's not terrible < 1268012086 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is using BabasChess < 1268012094 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Used to use Chess Machine and love it < 1268012242 0 :lament!unknown@unknown.invalid QUIT :*.net *.split < 1268012242 0 :HackEgo!unknown@unknown.invalid QUIT :*.net *.split < 1268012325 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268012399 0 :HackEgo!~HackEgo@codu.xen.prgmr.com JOIN :#esoteric < 1268012544 0 :bsmntbombdood!unknown@unknown.invalid PRIVMSG #esoteric :http://i.imgur.com/qlrHy.jpg < 1268012653 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :bsmntbombdood: OK, I'm putting that on sibeli.us for the moment. < 1268012760 0 :bsmntbombdood!unknown@unknown.invalid PRIVMSG #esoteric :i don't get it < 1268012854 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :http://sibeli.us/ < 1268012897 0 :bsmntbombdood!unknown@unknown.invalid PRIVMSG #esoteric :who the hell is Jean Sibelius < 1268012911 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :X_X < 1268012914 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :God I hate people. < 1268014135 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Anyone want to see the game between coppro and I? < 1268014225 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :??? < 1268014232 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Oh, chess game. < 1268014235 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I am so suck at chess. < 1268014665 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, bet you're better than me < 1268014674 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I haven't played in YEARS < 1268014680 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :And when I had, I barely paid attention < 1268014716 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I know the mechanics, just no strategy < 1268014732 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgoe: you were pretty good for the first half < 1268014737 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :but then your moves just became random < 1268014755 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :although you missed some opportunities to develop; getting pieces out and involved is key < 1268014834 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268014966 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric : hm... FAUST "Functional AUdio STream"... What are the chances of that name NOT being designed to fit the acronym? < 1268014992 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :exceedingly tiny i'd say, since if they didn't know about faust, FAST would have been closer < 1268015022 0 :coppro!unknown@unknown.invalid QUIT :Quit: I am leaving. You are about to explode. < 1268015050 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1268015214 0 :gm|lap!~gm@unaffiliated/greasemonkey JOIN :#esoteric < 1268017324 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: Awesome catch :P < 1268017373 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So, what person who's totally not me wants to get out the sheet music for Finlandia and record the event sequence for my Generic Music Idol Band Star Game. < 1268017378 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :With a "?" there < 1268017633 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :http://ficsgames.com/cgi-bin/show.cgi?ID=243952855;action=show < 1268017779 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1268017822 0 :Asztal!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1268019378 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1268019537 0 :gm|lap!unknown@unknown.invalid QUIT :Quit: HydraIRC is a child molester -> http://silverex.net/news <- i couldn't change my quit message < 1268019549 0 :GreaseMonkey!~gm@unaffiliated/greasemonkey JOIN :#esoteric < 1268019837 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :GreaseMonkey: Generic Music Idol Band Star Game? < 1268019838 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Erm. < 1268019842 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Generic Music Idol Band Star Game? < 1268019857 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Clearly, something *that* generic should have the sequence generated from the sheet music! < 1268019876 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Impossible, the recording, being of non-shitty music, doesn't have a constant tempo. < 1268019880 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... And by sheet music, I mean a convenient, easy-to-parse subset! < 1268019925 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION tries to think of non-shitty music with a constant tempo... < 1268019930 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is having severe difficulty. < 1268019973 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Okay, I'm having trouble thinking of *shitty* music with a constant tempo now. :P < 1268020063 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :4'33". < 1268020066 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION vejnas! < 1268020213 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ACTION plays zee5.ogg < 1268020216 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :;P < 1268020851 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Oh, I never really answered your question. < 1268020880 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Generic Music Idol Band Star Game is a generalization of DDR, Guitar Hero, Rock Band, and all the other identically dull games out there. < 1268020918 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Currently it's roughly equivalent to DDR, for the others I would need non-instant events, but that's a trivial addition really. < 1268020939 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And of course the horrendous karaoke part that should earn the death sentence to all who play it is excluded. < 1268021121 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Hey, DDR started it and was unique... < 1268021131 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... And then came more bemani from Konami... < 1268021131 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :DDR did not start it. < 1268021134 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And it was not unique. < 1268021139 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Parappa the Rapper started it. < 1268021154 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :DDR merely introduced a non-gamepad controller to the equation. < 1268021159 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... And then they started releasing games with just the music changed... < 1268021184 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And then Guitar Hero and Rock Band came around. < 1268021203 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Well after the genre had been beaten into a bloody, homogenous pulp. < 1268021248 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Regardless, DDR didn't start it, they were just the first ones clever enough to get people to pay for an alternate controller that is only useful for one game. < 1268021273 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Rock Band did the best in that regards of course, getting people to pay for FOUR alternate controllers that are only useful for one game, and are in fact interchangeable except for layout. < 1268021274 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :DDR's the home version of an arcade game. < 1268021312 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Well fine, they were the first ones clever enough to devise an alternate control mechanism, which they used initially in arcade :P < 1268021346 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Anyway, the whole genre is stupid rubbish that has the unfortunate tendency of making people think they have a viable skill when they have none. < 1268021380 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :But it's also an amusing thing to parody with Finlandia :P < 1268021384 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :DDR is quite enjoyable. But... Yeah, the whole genre is ridiculously repetitive. < 1268021397 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :"Oooh, let's make a new game, but with *different songs*!" < 1268021401 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Also, http://upload.wikimedia.org/wikipedia/en/4/4f/Inch_converter.jpg is the most horrifying thing I've ever seen. < 1268021416 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :"Hey, I got something better! Let's change the brand name and *have a different controller*!" < 1268021468 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And of course, no useful skill involved. Just a useless one. < 1268021598 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I suppose the basic agility encouraged by DDR is arguably a more viable skill than the ability to thumb something that's such a poor approximation of a guitar that it literally has no relevance were you to actually want to learn the guitar. < 1268021612 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Actually, hahahah, y'know what really started the genre? < 1268021616 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Miracle Piano Teaching System < 1268021631 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Also of note: DDR functions as a form of exercise. Everything else... Is about as useful as playing air guitar. < 1268021685 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :But Miracle Piano Teaching System is, of course, far too difficult for the average GMIBSGer, and besides it actually teaches a skill that borders on useful. < 1268021714 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Indeed. < 1268021750 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :At the least, you're more likely to impress a female with being able to play piano than being able to do Paranoia Survivor Max on challenge. < 1268021764 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And that is why all males do anything, right? :P < 1268021825 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :It's worked out well for me! >_> < 1268021836 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Hahah. < 1268021888 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :The karaoke-thing on Rock Band, tangentially, is damn near impossible if you can sing. < 1268021911 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :You're not allowed to use vibrato, yes? < 1268021919 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268021921 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Or rather, you'll be penalized for it. < 1268021924 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Or... Anything else. < 1268021939 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And God help you if you're not used to singing the melody. :P < 1268021946 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Heh < 1268021960 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :This is Rock BAND, not Rock CHOIR < 1268021991 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Although a choral GMIBSG would be ... impossible for the neanderthals that play that kind of game to figure out *shrugs* < 1268021996 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Feh, that was offensive. < 1268022003 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Neanderthals aren't so bad, really. < 1268022011 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :They're our cousins. < 1268022031 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Let's say ... australopithecus. < 1268022038 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Eh, most people play it as an excuse to be with friends. < 1268022046 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Kinda silly to need an excuse, but hey. < 1268022067 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I MIGHT have negative opinions about this genre of game :P < 1268022105 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I have negative opinions about most of the genre simply because it's been beaten in the ground more than even freaking sports games. < 1268022164 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Oh, and the choice of music for them usually *sucks*. < 1268022186 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Of course, they need the most constant and dull music possible to make the game possible. < 1268022196 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Aside from the fact that if it was good, royalties would be too expensive. < 1268022218 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :DDR tends to commission music. < 1268022231 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And Guitar Hero commissions... Covers. < 1268022239 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268022242 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Very annoyingly poor covers, too. < 1268022254 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :The whole concept of covers amuses me a lot, btw. < 1268022274 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It is kind of amusing, yes. < 1268022276 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I want to convince my cellist friend to say he's doing a cover of Shostakovich some time :P < 1268022316 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :All because of the singer-songwriter thing that started getting common in the 50s... < 1268022372 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION got reminded of that terrible Kansas cover again. < 1268022377 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :But what's really hilarious is that I'm sure that the majority of singer-songwriters nowadays are not, in fact songwriters, but the actual songwriters are grunts who get no recognition. < 1268022399 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: The majority of *popular* ones, perhaps. < 1268022408 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Naturally that's what I'm referring to, yes. < 1268022418 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :The popular singer-songwriters today aren't even singers. They're boobs with autotuners. < 1268022419 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :When you get outside the realm of popular musical shovelware, then you start seeing talent. < 1268022445 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Heck, just get outside the past couple decades or so and you start seeing talented people that are popular. < 1268022470 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So, you're saying that music continues its steady slide into the abyss :P < 1268022471 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Freaking autotune. < 1268022491 0 :Oranjer!~HP_Admini@adsl-71-7-92.cae.bellsouth.net JOIN :#esoteric < 1268022500 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Nah, just the stuff that gets shoved down people's throats that I'm not sure how anybody can like. < 1268022510 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :what what < 1268022519 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Awesome timing for Oranjer to waltz in :P < 1268022549 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :I'm guessing it's...religion? < 1268022566 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :No. < 1268022572 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Not particularly close. < 1268022572 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :darn < 1268022575 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Could be farther though. < 1268022576 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :I give up < 1268022588 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :There are logs, y'know :P < 1268022593 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :hmph < 1268022593 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Music. Specifically, manufactured music produced by the RIAA. < 1268022602 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1268022623 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Examples include Celine Dion and Nickleback. < 1268022625 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(effin' Canada!) < 1268022635 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Celine Dion is a national treasure < 1268022650 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Boobs with an autotuner. < 1268022664 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :boobs with an autotuner is a national treasure < 1268022672 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I beg to differ. < 1268022673 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Y'know, if they built the autotuner right into the breast implants, they could save a lot of trouble. < 1268022682 0 :GreaseMonkey!unknown@unknown.invalid PRIVMSG #esoteric :boobs with an autotuner is national treasure < 1268022692 0 :GreaseMonkey!unknown@unknown.invalid PRIVMSG #esoteric :(alt title) < 1268022730 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :in soviet russia, blah blah... < 1268022777 0 :GreaseMonkey!unknown@unknown.invalid PRIVMSG #esoteric :http://pubacc.wilcox-tech.com/~greaser/mods/dootman.it if you're lacking somewhat interesting music < 1268022784 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :You want a national treasure? *Jimi Hendrix* is a national treasure. < 1268022819 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :I agree < 1268023327 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :jimi hendrix is dead. < 1268023334 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :he can't be a national treasure. < 1268023345 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :augur: WE WORSHIP HIS BONES. < 1268023348 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :don't you get it, augur? < 1268023354 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :his bones have gone missing < 1268023356 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :oic < 1268023363 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :we have to go on a quest to find them < 1268023366 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :well, ofcourse his bones have gone missing < 1268023374 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :he's been resurrected < 1268023425 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :As a ZOMBIE < 1268023461 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :National Treasure 3: Zombie Hendrix would be, literally, the best movie conceivable < 1268023508 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Why 3? < 1268023511 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Ohwait < 1268023519 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :hahahaha < 1268023521 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :There were some movies called "National Treasure", weren't there? < 1268023527 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :yep < 1268023529 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yeah. < 1268023538 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Clearly not movies I ever saw :P < 1268023787 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :They weren't... Notable. < 1268023957 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :o.O at coppro's record on ficsgames.com < 1268023962 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Although it's better than mine < 1268024021 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :the first info I see on that site is entirely opaque < 1268024027 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :what is FICS? < 1268024064 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :hey! alright! < 1268024070 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Free Internet Chess Server [ freechess.org ] < 1268024070 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :does this handle variants? < 1268024091 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Some < 1268024093 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yes. < 1268024096 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :>:( < 1268024101 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :some does not mean any < 1268024105 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Oranjer finds a Chess server, and his first thought is "let's NOT play the game that we've been playing for thousands of years" < 1268024108 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :which means you can't define your own < 1268024122 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :well, that's my first thought with anything ever, so yay! < 1268024126 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :(OK, not thousands ;) ) < 1268024166 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Well, there's some ability to define your own starting positions I think < 1268024185 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: don't look there :P < 1268024188 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :hmph < 1268024313 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It'd be nice if it did shogi... < 1268024335 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AND GO < 1268024339 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And Poker < 1268024344 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And Checkers < 1268024344 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :isn't there a program out there that lets you play any chess variant? < 1268024351 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :including chess and go, I think < 1268024355 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :1,000...something, I think < 1268024397 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Shogi is a chess-family game. < 1268024429 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :damn, I finally found the program < 1268024437 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :but it costs money < 1268024447 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :http://www.zillions-of-games.com/ < 1268024459 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: I was being intentionally stupid :P < 1268024482 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :http://www.chessvariants.org/programs.dir/zillions/ < 1268024486 0 :Gracenotes!~person@wikipedia/Gracenotes JOIN :#esoteric < 1268024498 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Mmkay. < 1268024962 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION should probably do something that will give him nutrition < 1268025843 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :FICS has a number of popular variants, but nothing like new pieces < 1268025883 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I reluctantly admit, after much time using Firefox, that Chrome is a far more reliable browser >_> < 1268025892 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :The client-server model makes that difficult < 1268025903 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :yeah, Firefox gets major slops for reliability < 1268025912 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Why is it that flash stalls out and shits out Firefox, but in Chrome it doesn't? How does the process separation stop Flash from stalling? < 1268025973 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :that question seems obvious to me--but I fear that in asking it, you suggest a deeper answer? < 1268026010 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes, I do :P < 1268026024 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1268026036 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: When Flash stalls in Firefox, Firefox shits itself. < 1268026046 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :When Flash stalls in Chrome, Chrome kills the process. < 1268026069 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I'm not referring to halting or crashing, just momentary stalls. < 1268026076 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Ah. < 1268026096 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :That's just because Firefox's implementation of the NSAPI sucks. < 1268026098 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :e.g. Hulu plays seamlessly in Chrome, but is gappy and shitty in Firefox. < 1268026172 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :ACTION tries installing Chromiumn < 1268026329 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Chromeyfox < 1268026451 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I love Chrome < 1268026480 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I just trust Google's intentions less and less recently ... < 1268026499 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :shh! don't let them hear you! < 1268026511 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Google IRC? well then < 1268026532 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :You can always download SRWare Iron < 1268026542 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :>.> < 1268026554 0 :oklokok!unknown@unknown.invalid QUIT :Ping timeout: 248 seconds < 1268026584 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :there is a popup < 1268026587 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :I can't trust it boo < 1268026956 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Chromium is probably in your package manager. < 1268026970 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes, yes it is. < 1268026976 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :There. < 1268026984 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :That would be how I installed it. < 1268026995 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Why that's not Chrome. < 1268026999 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Has none of the nasty bits. < 1268027006 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :??? < 1268027025 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I thought Chromium was the devel name < 1268027073 0 :oklokok!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268027081 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :OKLOCOCK < 1268027325 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION has a chair! < 1268027666 0 :oklokok!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268028352 0 :oklokok!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268028889 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Chrome takes ages to compile. < 1268029220 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :g++ chrome.cc -lages -o chrome < 1268029530 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ACTION looks for a theme for Chrome called something along the lines of "Not being wildly different from the OS for the sole purpose of being wildly different from the OS, with no UI benefit" < 1268029744 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Now I'm waiting on the code going into /usr/src/debug. Hooray. < 1268029765 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(... So I like the ability to use gdb when something segfaults...) < 1268030093 0 :sebbu2!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268030094 0 :sebbu!~sebbu@ADijon-152-1-3-21.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1268030095 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :hi all < 1268030116 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :hello < 1268030437 0 :MizardX!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268030792 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :How does http://www.geocities.com/lifemasteraj/beginner1.html still exist? < 1268030870 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :What universe do these people come from? http://www.mywot.com/en/scorecard/geocities.com < 1268030884 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo, this is mind boggling < 1268030903 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :The WOT stuff, or the continued presense of the geocities site> < 1268030904 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268030917 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :latter < 1268031137 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Good lord, it's so Geocities too X-D < 1268031212 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Maybe e's paying for hosting? < 1268031869 0 :tombom!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1268032214 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1268034524 0 :tombom!unknown@unknown.invalid QUIT :Quit: Leaving < 1268035199 0 :clog!unknown@unknown.invalid QUIT :ended < 1268035200 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1268036184 0 :GreaseMonkey!unknown@unknown.invalid QUIT :Quit: HydraIRC -> http://www.hydrairc.org <- Nobody cares enough to cybersquat it < 1268037497 0 :cmeme!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1268037973 0 :sebbu!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1268038041 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 248 seconds < 1268038113 0 :cheater2!~cheater@ip-80-226-44-25.vodafone-net.de JOIN :#esoteric < 1268038228 0 :sebbu!~sebbu@ADijon-152-1-45-157.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1268038670 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1268039485 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1268041853 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1268041929 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1268043435 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268044861 0 :ais523!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268045425 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1268051190 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1268051407 0 :alise!~d4b78c00@gateway/web/freenode/x-znuyafmidzegrclp JOIN :#esoteric < 1268051410 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :16:08:17 so for T, P(L) -> (forall l, [] P l -> P(B l)) -> forall t, P(t) < 1268051416 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :sorry, had already left at that point < 1268051548 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'll play anyone at chess! Extremely badly! < 1268051706 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: hmm, I used to be OK at chess, but haven't practiced in years < 1268051722 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :major issue for me would be finding a chessboard that doesn't automatically suggest moves for me < 1268051733 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I've been beaten by a non-prodigy twelve year old. < 1268051735 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So... yeah. < 1268051754 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :tell you what, I think my really awful chess AI still runs in DOSBox < 1268051766 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: there are billions of clients for FICS < 1268051773 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I know < 1268051774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo and coppro played yesterday, see logs for what clients they used < 1268051797 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oh, I just assumed each player would use their own board and you'd send moves over IRC < 1268051890 0 :MigoMipo!~MigoMipo@84-217-1-84.tn.glocalnet.net JOIN :#esoteric < 1268051897 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ah; i have no chessboard at all here < 1268051909 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :chess sux < 1268051910 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ugh, it seems that although it runs in DOSbox, it captures both the keyboard and mouse < 1268051922 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and, also, I'm so bad it'd take me ages to figure out how to express the moves I make :-) < 1268051924 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :thus making it impossible to switch windows, or otherwise communicate with people < 1268051925 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :maybe I could use a program and you could use a real board < 1268051939 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: I meant, setting something like GNU chess to 2-player mode to use it as a board < 1268051947 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268051957 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :or we could just sign up for fics :P < 1268051974 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and have my horrible failure recorded for all eternity < 1268051986 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, almost works in wineconsole < 1268051994 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :only issue is that it sizes the screen incorrectly < 1268052010 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric : fixme:int:DOSVM_Int10Handler Load ROM 8x8 Double Dot Patterns - Not Supported < 1268052035 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, and that one shouldn't even be hard, you can simply implement it by doubling the vertical height of the screen < 1268052044 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :(virtual screen, that is) < 1268052046 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in fact, i'm sure someone must have made a java applet client for fics < 1268052057 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yeah but wine is shit :P < 1268052074 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :let's get crysis 5 working! who cares about the rest of the api < 1268052089 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :we want to support the gaymen community :| < 1268052098 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :meh, running a program and only 2 fixmes, that's not bad < 1268052111 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :besides, I've run stuff in WINE that I really needed to be able to run in order to get projects done < 1268052133 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it works just fine on MPLAB C30, except that it makes MPLAB spout a few warnings when it loads < 1268052137 0 :Quadrescence!unknown@unknown.invalid PRIVMSG #esoteric :alise: http://i.imgur.com/pDiHb.jpg < 1268052332 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :A-anyway. < 1268052527 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: fics or manual? I have the fics regpage up here < 1268052545 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :manual, because playing games over a work connection is hard to explain < 1268052573 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but I'm assuming attempting to keep track of everything said on IRC would be a fool's errand < 1268052615 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Just make a +m channel for it < 1268052626 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :you're disrupting one of my essential tactics! (decide what to do instinctively so that every move takes about a second) :-P < 1268052629 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Or did you mean the lack of even a local chessboard < 1268052652 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: also, the irc bytes sent and the chess bytes sent will be pretty much identical, you know < 1268052659 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in fact, the chess bytes may be binary and thus more obscure < 1268052675 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: the chess bytes will have headers < 1268052688 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and won't go through at all if they're on a nonstandard port < 1268052694 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you can automatically see where the bytes are sent < 1268052735 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ACTION googles for chess over irc out of curiosity; maybe there's something that'll automate it for me < 1268052755 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :If you have irssi there is < 1268052762 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Don't know about other clients < 1268052777 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :(And I haven't tried the irssi one either, I just know about it) < 1268052836 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :yeah i saw that but i meant a chessboard program that actually sends and recvs the moves itself < 1268052837 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ah well < 1268053210 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I can play if you want < 1268053347 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268053400 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: I can't decide whether you'd be better or worse than ais523 < 1268053432 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :well, I have no idea how good Deewiant is at chess; I'm formerly-decent-but-out-of-practice < 1268053443 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :maybe in the top 2 or 3 in the school while I was at secondary school < 1268053448 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I'm rather surprised how little this stock Windows 7 is annoying me < 1268053451 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :even IE8 < 1268053464 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I'm formerly-not-entirely-shit-but-out-of-practice < 1268053468 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I mean, sure, it sucks, but.. < 1268053478 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Load, you fucking downloa page! < 1268053478 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :IE8 is so much better than IE6, that's why it feels so good < 1268053479 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*download < 1268053482 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I want my chess client. < 1268053492 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: I know, but I keep forgetting I'm actually using IE as opposed to, say, Firefox < 1268053526 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and I actually really like using the taskbar to switch tab < 1268053527 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :s < 1268053527 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :without extensions, there aren't many user-visible differences between even IE7 and Firefox < 1268053537 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*tabs < 1268053539 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :also, taskbar to switch tabs would be a nightmare the way I use tabs < 1268053578 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but the thing is, I use alt-tab to switch windows mostly < 1268053582 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so it's actually quite nice < 1268053630 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ACTION tries to figure out how to get winboard to do two-player < 1268053654 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Our secondary school -equivalent had folks who got silver in some Scandinavian chess championship; at least one of the guys had an ELO near 2000 < 1268053701 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Probably all the active chess club people there (maybe 10-20 of them?) could beat me without too much trouble < 1268053717 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :This seems to not do two-player offline. Sigh. < 1268053730 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Just use FICS :-P < 1268053737 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Winboard works offline < 1268053737 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you could probably have written a chess client yourself by now < 1268053751 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: ais523 refuses to because of work connection < 1268053755 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I used to write them for practice when I was younger; I think I wrote one in Excel < 1268053759 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :also it does, but only one-player-against-engine < 1268053760 0 :Asztal!~asztal@host86-159-105-237.range86-159.btcentralplus.com JOIN :#esoteric < 1268053767 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :alise: Yes, but if you want to play me instead ;-) < 1268053776 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :alise: And no, there's mode -> edit game < 1268053783 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Last chance before I cruelly cast you aside in favour of a real man < 1268053788 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Which is basically equivalent to two-player one-machine < 1268053796 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise: last chance to what? < 1268053801 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Except that it doesn't have timing < 1268053802 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I don't mind not playing if it's too hard to set up < 1268053816 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: "edit game", what a ridiculous name for it! < 1268053820 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Well, use FICS or I cast you aside for now :P < 1268053830 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Well, it's not really a two-player mode. < 1268053854 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: do I need to register for fickz? < 1268053855 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :It's just that: allowing you to edit what move is taken at a given point. Something you'd typically do when viewing an already played game. < 1268053865 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :alise: I don't know how it works. :-P < 1268053871 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :That could make future moves impossible, surely? < 1268053874 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: >_< < 1268053888 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Well, surely it deletes the history from that point forward. < 1268053892 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : If you are not a registered player, enter guest or a unique ID. < 1268053915 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :"alise" is not a registered name. You may use this name to play unrated games. < 1268053917 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Right. < 1268053919 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Well, connect. < 1268053928 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I am connected, I even registered. < 1268053939 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :could we have the moves posted in-channel somewhere so I can watch? < 1268053947 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :maybe not this channel, though < 1268053955 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Easy enough < 1268053956 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Okay. < 1268053964 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :#deewiant-alise-champ-2010 < 1268053968 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268054321 0 :alise_!~d4b78c04@gateway/web/freenode/x-slkqghjzttivkkpe JOIN :#esoteric < 1268054442 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268054913 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1268056202 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268060518 0 :cpressey!~CPressey@173-9-215-173-Illinois.hfc.comcastbusiness.net JOIN :#esoteric < 1268062893 0 :alise!~d4b78c36@gateway/web/freenode/x-wjnbxpftbetytfdo JOIN :#esoteric < 1268062915 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Name for a Reversi-playing program: Infersi < 1268063032 0 :coppro!unknown@unknown.invalid QUIT :Quit: I am leaving. You are about to explode. < 1268063065 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :coppro's quit message has been false every time so far < 1268063072 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'm starting to suspect he doesn't actually mean it < 1268063084 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :either that, or it isn't targeted at me, in which case some context would be helpful < 1268063117 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I've exploded several times when he's left < 1268063131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Quite painful < 1268063257 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I wonder what the most practical Haskelly thing is for making a GUI < 1268063277 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I have no idea, but deep-down I hope it indirectly involves Befunge < 1268063341 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Write Befunge code that uses WIND and then system "rcfunge tmp.b98" ? < 1268063383 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :No < 1268063384 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :something like that, but with more tight binding on the Haskell < 1268063391 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :maybe you could go via INTERCAL < 1268063391 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Also, that's Windows-only < 1268063404 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :if INTERCAL doesn't have Haskell bindings yet, it probably should do < 1268063421 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :mostly to annoy Haskell advocates < 1268063432 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :alise: What's Windows-only? WIND is only implemented using X < 1268063455 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I would prefer something written in pure Befunge that uses ANSI control codes to make a ncurses-y user interface < 1268063455 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Or at least, RC/Funge-98 only implements it with X, and I don't know of any other interpreter that implements it at all < 1268063457 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Okay. < 1268063457 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Oh, really? < 1268063488 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :RC/Funge-98 is very non-Windows-only < 1268063494 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Quite the opposite < 1268063500 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it would be funnier if the software only worked using X on Windows < 1268063523 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268063524 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: yep, and that sort of thing's entirely possible; I just don't think anyone's tried yet < 1268063541 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : I would prefer something written in pure Befunge that uses ANSI control codes to make a ncurses-y user interface <-- anything wrong with NCRS? < 1268063553 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :for a start "something written in befunge" tends to be very non-reusable < 1268063565 0 :alise_!~d4b78c36@gateway/web/freenode/x-muhpxrmaljweggxk JOIN :#esoteric < 1268063579 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :due to the complete lack of something that works for emulating functions. And even with SUBR it is somewhat messy < 1268063669 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Don't forget MACR < 1268063726 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268063794 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, is there any Befunge extension that works Modular SNUSP-style? < 1268063829 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Depends on what that style is < 1268063891 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :basically, it has commands for subroutine call and return < 1268063901 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that work like setjmp/longjmp on an explicit stack < 1268063990 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I don't think there's anything quite like that, no < 1268064046 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it makes subroutining very easy < 1268064053 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :or ofc you could just use IFFI and do subroutines that way < 1268064117 0 :MissPiggy!~none@unaffiliated/fax JOIN :#esoteric < 1268064127 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant, hm... < 1268064140 0 :MissPiggy!unknown@unknown.invalid NICK :fax < 1268064156 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, you need to port IFFI to work without depending on ick < 1268064168 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :At one point I wanted to have "pages" that the IP could travel between (kind of like 2.5 dimensions I guess), but there was a lot of resistance (too machine-y, I guess.) < 1268064169 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :that would be "rewrite", not "port" < 1268064172 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :of course, since you replace mainloop that would be painful < 1268064173 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :but it's a useful project < 1268064186 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, also, it must work with t < 1268064190 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :unlike IFFI currently < 1268064190 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the replacing the mainloop is actually not an issue, it's a trivial wrapper < 1268064209 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :the real issue is that it's tightly hooked to ick's control logic, on the basis that the entire purpose of CFFI is to do that < 1268064223 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, I think I joked about a two letter fingerprint NX. That works like the page permissions on hardware < 1268064232 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268064233 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :read, write, execute flags < 1268064243 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I'm not sure what a write only area would be useful for < 1268064255 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :logging? < 1268064267 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, would be easy to overwrite what you logged though < 1268064267 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :you could read it in a debugger, but not make a security leak < 1268064279 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, I'm not sure that makes sense < 1268064285 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :since other threads could still read the data < 1268064286 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Something more elegant would be some kind of "memory switch" that remembers which direction you turned (i.e. which branch you took), and lets you reverse it / backtrack... that captures the idea of call/return but in a kind of spatial way. < 1268064303 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: MODE has switchmode which is essentially that. < 1268064320 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: sounds worryingly like TRDS < 1268064337 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :which could also be very usable for subroutine call/return, if it wasn't for the essential complexity of the whole thing < 1268064338 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Although of course it doesn't work with multiple threads. < 1268064360 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Since it only remembers the latest branch ever, not the latest branch per IP. < 1268064417 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :huh < 1268064525 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Switchmode is close, but it would need to be more elegant, combining in the functionality of w, perhaps. < 1268064574 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :What to do with a w that passed through? < 1268064578 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I.e. compared equal < 1268064588 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Otoh, pretty dispatcher structures are one of the things that make Befunge fun, so why try to make it easy? < 1268064597 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :For the other cases, you can single-usely turn it into [] < 1268064635 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: You could turn the w into one of three instructions that reverses the decision and then turns itself back to w for the next use. < 1268064654 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :But what does reversing == mean < 1268064661 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Since it distinguishes between < and > ordinarily < 1268064667 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :You'd have to pick one arbitrarily? < 1268064688 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Reversing the path chosen. == chooses the straight line, reversing the straight line still is the straight line. < 1268064721 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I suppose so < 1268065209 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Speaking of "practicality" in esolangs I always liked the idea of an "esoteric OS adapter" (Easel/PESOIX/PSOX) much better than language-specific facilities like fingerprints. But it seems so much harder to get such a project off the ground. < 1268065280 0 :ais523!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268065306 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I think it's somewhat of an excuse to limit the capabilities of your esolang < 1268065372 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :I mean, all you need now is putchar and getchar and you're done; language-specific ways of talking to the OS/doing other things like that can be more interesting, IMO. < 1268065410 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :They can be, true. < 1268066212 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1268066282 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :07:43:52 --- quit: coppro (Quit: I am leaving. You are about to explode.) < 1268066283 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :07:44:25 coppro's quit message has been false every time so far < 1268066298 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well in the long run, if the Big Rip hypothesis is true... < 1268066777 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I mean, PSOX is in no way a replacement for Befunge fingerprints, because those can affect the language, not just the OS. But there are just so many esolangs out there that just can't be reasonably expected to grow their own OS features. (Not that PSOX would necessarily be able to help all of those, either, though) < 1268066881 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I think the big barriers to adoption are 1) the spec isn't simple/abstract enough and 2) there is no proof of concept implementation < 1268066892 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :(Isn't that always the story, though?) < 1268066973 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I would like to stand corrected about there not being an implementation < 1268067004 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo does seem to have an implementation of it in Python? < 1268067032 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :The file I/O stuff needs some work < 1268067046 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :And the spec for the File I/O stuff is probably iffy < 1268067348 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Also, it's untested on Windows < 1268067367 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Although was a major spec change just due to projected issues with Windows < 1268067547 0 :kar8nga!~kar8nga@jol13-1-82-66-176-74.fbx.proxad.net JOIN :#esoteric < 1268067640 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Having it be a pipeline (and only a pipeline) is definitely the right design, I think. < 1268067678 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I haven't unravelled the spec sufficiently to know what I think about the details yet... < 1268069551 0 :tombom!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1268069758 0 :hiato!~fdulu@dsl-245-10-22.telkomadsl.co.za JOIN :#esoteric < 1268069932 0 :hiato!unknown@unknown.invalid NICK :sudobus < 1268069984 0 :sudobus!unknown@unknown.invalid NICK :aqualoqua < 1268069995 0 :aqualoqua!unknown@unknown.invalid NICK :sudobus < 1268070034 0 :sudobus!unknown@unknown.invalid PART #esoteric :? < 1268070317 0 :hiato!~fdulu@dsl-245-10-22.telkomadsl.co.za JOIN :#esoteric < 1268070323 0 :hiato!unknown@unknown.invalid NICK :sudobus < 1268071294 0 :alise!~d4b78c25@gateway/web/freenode/x-sbcmzggvryvggwvj JOIN :#esoteric < 1268071337 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Chromium is the devel name < 1268071342 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and all the nasty stuff has options to disab;e < 1268071343 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :so there < 1268071423 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: You can set chromium to use OS colours < 1268071430 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in options < 1268071443 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1268071468 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268071574 0 :alise_!~d4b78c25@gateway/web/freenode/x-nfzwvdertqtqktst JOIN :#esoteric < 1268071579 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :21:35:32 You can always download SRWare Iron < 1268071583 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You could, but you'd be retarded: < 1268071600 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://neugierig.org/software/chromium/notes/2009/12/iron.html < 1268071690 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268071730 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... He was expecting *money* from that? < 1268071730 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Dear God. The money in FLOSS is... Support. < 1268071749 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: you're a fax machine again? < 1268071763 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: he got it - see all the publicity < 1268071771 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I especially like how he removed an entirely innocuous class < 1268071824 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise_: So. Dumb. < 1268071841 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :If he wanted a real privacy-based browser, he'd do... Something smarter. < 1268071852 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Default to incognito, integrate Tor, etc. < 1268071854 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Best thing to do is just to turn off all the settings in main Chrome. < 1268071866 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yuh. < 1268071874 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :They're settings for a reason, after all. < 1268071877 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Google Updater automatic installation. < 1268071882 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :automatic updates = privacy violation < 1268071890 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Bug tracking system, sends information about crashes or errors. < 1268071896 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :bug reporting = privacy violation < 1268071906 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :DNS pre-fetching. < 1268071909 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dun dun DUNNNN < 1268071916 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A timestamp of when the browser was installed. < 1268071920 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Oh now /that/ is just insidious < 1268071950 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm just surprised how candid he was about his real goal < 1268071956 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :;) < 1268071957 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :DNS pre-fetching was even *called* insidious? < 1268071960 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :;);););) < 1268071966 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: oh the lines that aren't factual are my mocking < 1268071972 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the guy clearly has no idea what he's doing < 1268071993 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I submit that he knows exactly what he is doing < 1268071997 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i read the full log he doesn't understand why people aren't nice to him :-) < 1268071998 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :He's marketing < 1268071999 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: i mean code-wise < 1268072011 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Ah. Well there, he barely needs to < 1268072020 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Also: what means rotful? < 1268072033 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Only needs an understanding of what will scare sufficiently paranoid people < 1268072039 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :We haven't had a super-shitty #esoteric meme in ages, and we need one. < 1268072057 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :rotful < 1268072058 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1268072066 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: yo < 1268072082 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: wow, my brain has completely different heuristic clauses for MissPiggy and fax < 1268072099 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: so I actually read that "hi" completely differently than if you said it before changing your nick back < 1268072113 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :apparently my brain infers huge gobs of meaning into "hi" purely based on who says it < 1268072119 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::) < 1268072146 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :permanent nick change or not? < 1268072191 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise_: ... Mine too, oddly enough. < 1268072227 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm... i guess it will take some time for the heuristics to migrate < 1268072239 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :unless you're going to start acting like fax acted too, in which case you'll be two entirely different people < 1268072318 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: The issue with PSOX was basically that Sgeo didn't know what he was doing, so it was in fact rather heavily Brainfuck-oriented. < 1268072377 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(and Linux) < 1268072391 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Obviously the solution is to have it communicate with /its own/ esolang that just does IO stuff. < 1268072402 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :PSOX seems mostly alright. There are definitely some things that need clarification, and some that I would want to change. < 1268072410 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*disable (typo from way back) < 1268072429 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Well, it only works with languages that do unrestricted byte-by-byte two-way synchronised binary IO. < 1268072431 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Which is ludicrous. < 1268072436 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :| | | < 1268072436 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :+-+ * | < 1268072436 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :| | | * < 1268072482 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wat < 1268072486 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: But that's common. If your language communicates with smoke signals, anything like PSOX isn't going to be much help anyway. < 1268072503 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Well, printable ASCII would be a good subset to use... < 1268072508 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :It looks line-oriented, actually. < 1268072516 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's still heavily binary. < 1268072521 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Also, it's abandoned. I forget why. < 1268072538 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Printable ASCII I could live with, but I don't know of any langs that are really crippled from binary I/O? < 1268072552 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :That's more of an OS issue. < 1268072556 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Thank you, MS-DOS. < 1268072556 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If I were going to spec an IO esolang, I would have it use little particles of data being catapulted off to data sinks (forts), and "enemy" cannons (input sources) shooting out particles. < 1268072566 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So you place forts and cannons in the right place to aim, and coordinate their firings. < 1268072575 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: INTERCAL-72 can only do roman numerals < 1268072579 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :alise_: OS /colors/ are not the issue. OS /style/ is the issue. < 1268072598 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so perhaps INTERCAL-72 roman numeral format without over/underlines (so only small numbers) is the lowest common denominator < 1268072606 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Well, you can get the title bar. And it uses GTK widgets inside the page. < 1268072633 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: If that isn't acceptable, don't use Chrome :P < 1268072636 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: It could look for the first two symbols output, consider them '0' and '1' in binary, and build the rest on that. < 1268072638 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :If it uses GTK widgets, then why even with "use GTK+ theme" (whatever that means) enabled does it look like friggin' Windows >_< < 1268072650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Use GTK+ theme = use its colours < 1268072657 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :And because you don't have a GTK+ theme set up, presumably. < 1268072660 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So it's using Raleigh. < 1268072664 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Which looks uber-ugly. < 1268072667 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I use XFCE. < 1268072674 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So I most certainly have a GTK+ theme set up. < 1268072679 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Then it's because you touch yourself at night. < 1268072694 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :More seriously, it's because it's using your title bar colour for a big bit, I imagine. < 1268072694 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I touch myself in broad daylight, thank you very much. < 1268072699 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You could try and edit the settings manually. < 1268072705 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If the 3rd character output is different from the first two, it could assume you have printable characters available... if it's non-printable, it could assume you have 0-255. < 1268072746 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: you might want it to use the first two _lines_ output < 1268072750 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: I think that for most esolangs, fancy programs are /boring/. < 1268072762 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :An IRC client in SNUSP. Whoopdedo, < 1268072767 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*Whoopdedoo, that's mostly glue. < 1268072778 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :For those where it can be interesting, it's because of an aspect of the language. < 1268072782 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So you want it part of the language. < 1268072984 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :That's along the lines of what I was thinking when I said PSOX makes stuff less interesting < 1268073045 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1268073055 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :ACTION shrugs < 1268073057 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :OK < 1268073118 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm certainly not looking to write a webserver in Hargfak. < 1268073155 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I was more thinking of it as a tool to allow esolangs to be more easily passed off as "real". < 1268073166 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :i.e. < 1268073168 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Marketing. < 1268073201 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But if it makes things less interesting, n/m < 1268073286 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But on that note, I don't see why most Befunge fingerprints are interesting. < 1268073428 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :They aren't. < 1268073436 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :In fact, Befunge is relatively uninteresting past its abstract core. < 1268073444 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Concurrency adds a large gob of fun. < 1268073456 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Time travel and multiverses add more large gobs. < 1268073457 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Beyond that, meh. < 1268073502 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :s/interesting/a popular topic of conversation/, then. < 1268073530 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Bad news! < 1268073533 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"Let me repeat that. By allowing the judgmental equality to identify these two closed extensionally equal values, we collapse the judgmental equality on terms under a false hypothesis. Bye bye typechecker." < 1268073539 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://www.e-pig.org/epilogue/?p=324 < 1268073552 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Because the hoi polloi suck at identifying the novel. < 1268073569 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :In fact all the fun in -98 is pretty much the huge sack of implementation woes. < 1268073570 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that post is quite confusing, I don't understand why this doesn't mean epigram is broken < 1268073579 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: it is < 1268073584 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :they're having to replace W-types with something else < 1268073598 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :otherwise they're fucked < 1268073627 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what confuses me is, whatever they replace W types with: Can't you just implement W with /that/? < 1268073645 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :obviously they have to replace it with something less powerful/abstract < 1268073654 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://muaddibspace.blogspot.com/2010/03/algebra-system.html you didn't tell me you had a blog :| < 1268073702 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: In that case, Befunge-111 should probably not exist. A clear, unambiguous spec would only ruin the fun. < 1268073709 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :because it's embarassing :P < 1268073719 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: lawl < 1268073729 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Well... yeah. Isn't that obvious? < 1268073739 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You need to introduce a bag of craziness to make it fun, which is why I've been pushing my idiocy. < 1268073747 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :No, not to me. < 1268073764 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: hmm... I agree that ZFC is probably inconsistent, yet I'm having some sort of knee-jerk AARGH NO reaction to its statement < 1268073773 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Help? < 1268073785 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268073829 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I think I've read a post on your blog before and it was ridiculously overcomplicated for something < 1268073858 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :mm? < 1268073859 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :What's this about ZFC being inconsistent? < 1268073875 0 :MizardX!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268073880 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: it probably is < 1268073923 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :That would be News. < 1268073923 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://r6.ca/blog/20091101T231201Z.html < 1268073928 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :well, not probably < 1268073931 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1268073942 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but if you belong to general dependent-type constructivist cabal, then yeah probably :P < 1268073954 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: of course you forgot to add "for the same reasons that Coq is probably inconsistent". < 1268073959 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise: Today I just picked up "Constructive Functional Analysis" < 1268073993 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"Can we really believe in the consistency of any system whose ordinal strength we do not have a notation for?" < 1268073995 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :... < 1268074009 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION can't interpret that '...' < 1268074009 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :...... < 1268074015 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :nor that < 1268074026 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Probably "That's ridiculous, either p or not p" < 1268074035 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(Note: Above sentence is merely mocking the mocking of the classicalists.) < 1268074093 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"..." was shorthand for "..." < 1268074094 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Ah yes, I think it was your thing on halving numbers < 1268074107 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I thought it might be that < 1268074115 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Inner meaning? < 1268074137 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Maybe I'll eventually figure out the words for the thought, but don't expect it soon. < 1268074207 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Fundamental thought, generalised, is "I agree", "I disagree" or ""? < 1268074242 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Honestly, my inclination was to respond with "Please, won't somebody think of the children??!?!" < 1268074248 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I don't think whether a person belongs to a general dependent-type constructivist cabal or not has any bearing on whether ZFC is probably inconsistent or not. < 1268074258 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: you object to insulting wolfram? :| < 1268074265 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But I am sensitive to overusing Simpsons quotes. < 1268074273 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :stop stalking me!! < 1268074277 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Oh yes it does! < 1268074281 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I CAN'T HELP IT < 1268074348 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hey gloss is exactly what i need for my othello program i think < 1268074353 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :can it do mouseclicks, I wonder < 1268074395 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm reading about finite calculus right now, though < 1268074421 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :the discrete derivative of f at x is defined as f(x+1)-f(x) < 1268074434 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :What would it mean for ZFC to be inconsistent? In practical terms, I mean. < 1268074474 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :It would mean that in ZFC, it's possible to prove anything at all, making all theorems proved in ZFC meaningless. < 1268074504 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Exactly. < 1268074531 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's probably easy to modify the axioms to make it consistent if it isn't, but you'd lose tons and tons of results. < 1268074531 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I was thinking more like, another refinement would be layered onto it to plug the hole, like ZFC itself was layered onto naive set theory. < 1268074542 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise you know I have a soft spot for people like wolfram < 1268074554 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I don't actually. < 1268074560 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1268074579 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I do. It's a beanbag chair in a dungeon. < 1268074587 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Personally, the way he reacted to ais523's solving of the Wolfram prize gives it a slightly personal edge to me. < 1268074621 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :"Oh, how wonderful! A kid has proved what I always suspected. This has wide-reaching implications and provides an important bit of evidence for MY unifying theory of everything. When I first wrote about it ..." < 1268074720 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :did he mistreat ais in some way? < 1268074828 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :He did him a great intellectual disservice by making only passing mention to his achievement in his post on it, and spending 99% of the large tome talking about how good he was for thinking of it. < 1268074894 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Even before I knew that, he rankled me immensely. < 1268075020 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Of course. I especially enjoyed the Usenet post where he, as a teenager, belittled someone with far more experience than him because he had a pile of books with which to learn more than him. < 1268075057 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Number of references to the body of computability research in "New Kind of Science": ... well, he mentions the name "Turing" a couple of times. In the phrase "Turing machine". < 1268075058 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :link? < 1268075068 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I'll find it; sec. < 1268075100 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: For now, he's Feynman writing to Wolfram (warning: surrounded with wolframlove by the transcriber) http://elzr.com/posts/wolfram-feynman < 1268075103 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*here's < 1268075226 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If ZFC was inconsistent, there would be chains of reasoning in it which did not terminate, correct? < 1268075236 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: You are thinking in computational terms. < 1268075243 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Inconsistency means that you can prove a falsehood. < 1268075252 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :This is a contradiction. < 1268075253 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: As is my perogative, I thought. < 1268075257 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i.e.: p & ~p. < 1268075267 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :From this, you can prove anything. < 1268075295 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You can prove that false is 42, that 43+1 = -99 and -99 is also a horse of size 98 that behaves as a monoidal functor when applied to itself. < 1268075296 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If you can prove anything, you can prove the premises, therefore there are chains of reasoning which do not terminate. < 1268075302 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :See http://xkcd.com/704/ for an example < 1268075323 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: I liked that xkcd - incredibly rare for me as of late. < 1268075349 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :xkcdsucks had a really stupid rebuttal saying that a piece of data isn't true or false, it's a piece of data, but obviously you'd just do "Your mom's phone number is 923487958" and prove that < 1268075350 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then use that < 1268075358 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268075408 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: In the dependent-types view, we hvae < 1268075411 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*have < 1268075415 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Types :: statements < 1268075417 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Values :: proofs < 1268075429 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :If you prove a falsehood, your value doesn't terminate when evaluated. < 1268075438 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :alise_: The most recent xkcd was REALLY bad. < 1268075441 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So, yes, in a way you are right. < 1268075442 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm not convinced of the converse, though (If there are chains of reasoning which don't terminate in ZFC, then it's inconsistent) < 1268075446 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So bad I may remove it from my RSS reader. < 1268075447 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But "termination" doesn't make any sense in logic. < 1268075451 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I don't read xkcd. < 1268075456 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Yeah, that was an enjoyable xkcd. < 1268075459 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Infinite chains of reasoning, perhaps, but there is no computation, so there is no termination. < 1268075469 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: I used to. < 1268075474 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :But it became shitty. < 1268075494 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: You have a computational view of "termination", I think. < 1268075494 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I read xkcd still because *following* a hit-and-miss comic takes very little time. < 1268075505 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Right you are. < 1268075510 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Once I've started following a comic, it takes a severe facepalm moment for me to stop. < 1268075515 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... Or just severe apathy. < 1268075517 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok, hi < 1268075541 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Yeah, but this latest one was terrible, even for XKCD. < 1268075546 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Like, ow, my brain hurts terrible. < 1268075633 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: what do you mean by "chain of reasoning"? < 1268075644 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: True. It did quite suck. < 1268075653 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :This looks like a non-terminating chain of reasoning to me: 1 = 1; therefore, 2 = 2; therefore, 3 = 3; therefore, 4 = 4; therefore, . . . < 1268075669 0 :alise!~d4b78c21@gateway/web/freenode/x-auikqbxrruntunxf JOIN :#esoteric < 1268075684 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Or just "1 = 1 therefore 1 = 1 therefore ..." < 1268075697 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: did you /see/ the xkcd where the whole joke was "Here are some cartoon female genitals. Here are stick people that cannot possibly possess them. LOL, TGI FRIDAYS" < 1268075723 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: ... I think I scrubbed it from my memory. < 1268075738 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: AFAICT that's what I mean. < 1268075757 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hey I've hated xkcd for years < 1268075759 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: okay, so I just showed you a non-terminating chain of reasoning. So does that mean ZFC is consistent? < 1268075760 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268075762 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :how come you guys are only just catching up now < 1268075762 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: imo proofs aren't actually part of zfc's truth space < 1268075774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: it started sucking around maybe 2007-2008 imo. < 1268075781 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :You have axioms and rules for deriving theorems from those axioms. < 1268075785 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: as in they're just a tool for us to reason about, and verify things < 1268075795 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :but they're totally orthogonal to any issue actually related to the set of truths we call zfc < 1268075796 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :fax: Because it's gone from overrated but amusing to overrated and sucking most of the time. < 1268075802 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268075839 0 :sudobus!unknown@unknown.invalid PRIVMSG #esoteric :ACTION liked it better when the convo was about stuff he knew about, like the cocio-economic effects of a potential utube cencorship, or cats < 1268075861 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: No, that's the converse that I said I wasn't convinced of, isn't it? < 1268075874 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"utube" ;_; < 1268075889 0 :sudobus!unknown@unknown.invalid PRIVMSG #esoteric :fax: (: < 1268075893 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :sudobus: you do realise this is a progrmaming channel :) < 1268075896 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :*programming < 1268075902 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric : I'm not convinced of the converse, though (If there are chains of reasoning which don't terminate in ZFC, then it's inconsistent) < 1268075913 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: so now are you convinced that the existence of a non-terminating chain of reasoning doesn't imply that it's inconsistent? < 1268075929 0 :sudobus!unknown@unknown.invalid PRIVMSG #esoteric :alise: sudobus == hiato < 1268075934 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: Other way 'round. If it's inconsistent, then etc < 1268075939 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :sudobus: Spelling. Improve it. < 1268075940 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268075953 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: he's south african he can do what the hell he likes because he's interesting < 1268075957 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :sudobus: I know what a catbus is, but what's a sudobus? < 1268075960 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :IRC has just enough people who spell things correctly to make it really depressing when someone comes out with shit like "cong@l8" < 1268075976 0 :sudobus!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Srue tihng man < 1268075985 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :rotful < 1268075986 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: here's wolfram being a complete idiot http://groups.google.com/group/comp.lang.lisp/msg/f3b93140c2f2e922?dmode=source&output=gplain&pli=1 < 1268076006 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I think you mean "çocio-economic" and "cençorship". < 1268076020 0 :sudobus!unknown@unknown.invalid PRIVMSG #esoteric :alise: it's what you get when you take a and rest it perpendicularly on a piece of paper that says "sudo" just right tos that the o's overlap < 1268076024 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Most people are complete idiots at least a couple of times in their lives < 1268076034 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I think he meant イエユイノボメノ. < 1268076037 0 :sudobus!unknown@unknown.invalid PRIVMSG #esoteric :uorygl: sorry, my bad < 1268076039 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :(note -- not actual Japanese) < 1268076040 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, ah this is KMP -- I have read this < 1268076045 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Yes, it takes a very special sort of person to make a career out of it. < 1268076057 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: kmp? < 1268076060 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :oh pitman < 1268076095 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :Indeed < 1268076127 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: It shows that Wolfram has a huge attitude problem & ego that has lasted til today. < 1268076130 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :He then said "I'm going to read these and then I'll know as much as you." < 1268076134 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hehe < 1268076146 0 :sudobus!unknown@unknown.invalid PRIVMSG #esoteric :alise: I just realised I left out at least a word from my previous reply. Note: rest a mirror ... just right so that the .. < 1268076215 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I actually am going to read these, and then I actually will know as much as you! < 1268076265 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I should carry about a stack of books just incase I want to insult someone < 1268076340 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :including "the compiler book with the dragon on it" < 1268076349 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: AAAH. < 1268076369 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Tangentially, I should read the Dragon Book sometime. < 1268076376 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why? it's outdated < 1268076383 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you would only read if you like history < 1268076390 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :What's not outdated? < 1268076398 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Appels book < 1268076399 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :... Outdated books can be enjoyable. < 1268076422 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Or at least enlightening. < 1268076446 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :fax: The latest edition of the dragon book is newer than Appel's < 1268076459 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :By about 10 years < 1268076460 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Oh, and there have been 2 later editions. < 1268076463 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Most recent was in 2006. < 1268076476 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Of course, most people think of the *first*, but still. < 1268076488 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ah that's interesting < 1268076500 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :they have republished it, I have not seen the new version < 1268076501 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :The first is out of print :-P < 1268076508 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I've heard the recent editions are not much more than reprints of the originals? < 1268076511 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant: Yeah, yeah. < 1268076516 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :there aren't any compiler books from a functional perspective < 1268076517 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hmph < 1268076533 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :alise: "Modern Compiler Design" explains a bit of how Haskell is compiled < 1268076538 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise: "Modern Compier Design"... yeah < 1268076544 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :no, I mean < 1268076548 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :structuring compilers functionally < 1268076552 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, Calculating Compilers < 1268076552 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :MCD's coverage is not very good though < 1268076564 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(PhD thesis, but it's a good read anyway) < 1268076567 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: well... foo to you < 1268076570 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: True, unfortunately < 1268076571 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: The Implementation of Functional Programming Languages, by SPJ? < 1268076576 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :foo ?? < 1268076596 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Part of me wonders why you even need a book on it :/ < 1268076597 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, http://www.reddit.com/r/squiggol/ < 1268076606 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Sexy purposes < 1268076672 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise??? < 1268076674 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Gah < 1268076680 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://www.uni-koblenz.de/~laemmel/expression/long.pdf cool, material on the expression problem! < 1268076683 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Proving compilers correct is useless. < 1268076693 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, hahahahah < 1268076693 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Prove the generated code is correct. < 1268076700 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: That's... what you do. < 1268076728 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: ... That's not the only reason to write a compiler functionally... < 1268076734 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Or write anything functionally... < 1268076735 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :A correct compiler will take an incorrect program and produce another incorrect program. < 1268076737 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You prove that the canonical semantics of the input (syntax tree) are equivalent to the canonical semantics of the output. < 1268076739 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"Proving compilers correct is useless." -- I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a remark. < 1268076745 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :And... That's... What people do... < 1268076745 0 :sudobus!unknown@unknown.invalid QUIT :Quit: leaving < 1268076763 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: Some of it is overstatement. But not all of it. < 1268076765 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Why yes. Yes it will. < 1268076774 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Adapted from Babbage - On two occasions I have been asked, 'Pray, Mr. Babbage, if you put into the machine wrong figures, will the right answers come out?' I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question. < 1268076785 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: And I would expect nothing more of a correct compiler. < 1268076800 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Well. I also want correct code to produce correct output. < 1268076823 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So, dependently-typed combinator calculus. < 1268076833 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :... < 1268076837 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Specifically: a language with only combinators that has dependent types and is total (but not powerless). < 1268076841 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(No lambda abstractions.) < 1268076843 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise answer me! < 1268076844 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :A compiler is code. Proving a compiler correct is a subset of proving code is correct. Why people concentrate on that one subclass eludes me. < 1268076844 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Commence. < 1268076848 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: answer WHAT < 1268076852 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :s/sub*/subcase/. < 1268076862 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise from earlier < 1268076865 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Uh? < 1268076872 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: what < 1268076912 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: It's fairly simple -- when your compiler is *incorrect*, you cannot rely on the compiler to generate correct code. < 1268076921 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ugh alise why are you so mean < 1268076930 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: I'm not, I just don't know what the fuck you want me to do < 1268076950 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Please stop assuming you're the center of the universe and that I follow what you say above all others, I like you but please just repeat what you want me to reply to < 1268076999 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Proving a compiler correct is proving a function (Lang -> Lang) correct. Call it f. What you're saying is "Prove that semantics (f x) = semantics x". But if we wanted to prove f correct, we have to express the intended semantics. "Given the input x and the output x', prove that semantics x' = semantics x". < 1268077006 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Right, so proving programs correct is important. I get that. < 1268077011 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :So proving the compiler correct /is/ proving the compiler's output correct. < 1268077023 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :What I don't get is why this *special case* is so friggin' popular, esp. in theses. < 1268077049 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because it's hard. < 1268077050 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :and important < 1268077052 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, you just seem to sort of phase out when I link you stuff < 1268077055 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :see e.g. Reflections on Trusting Trust < 1268077063 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Because it's more important than most other cases. < 1268077065 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: no I just don't respond to links that I am unable to interpret the context of; also, I did respond < 1268077069 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I linked to an article linked to in that subreddit < 1268077073 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Since almost everything is compiled. < 1268077081 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, no there's a compilers book in there < 1268077095 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: i didn't see < 1268077101 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1268077104 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Yet ultimately, everything is interpreted. < 1268077123 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :We should probably be proving our text editors correct, too. < 1268077232 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Do you have any idea how much verification goes into making an x86 CPU? < 1268077233 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, http://jaguar.it.miami.edu/~chris/formal_methods_in_the_movies/TheWizardOfOz.html < 1268077277 0 :alise_!~d4b78c21@gateway/web/freenode/x-scxeyrkywnvjhjyu JOIN :#esoteric < 1268077284 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise: Issues still slip on through on occasion, though. < 1268077295 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Though the only such case I can think of is the FDIV bug on the Pentiums... < 1268077308 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: We do not prove our editors correct because it is incredibly trivial to verify that they produce the correct results with a so-simple-there-cannot-be-any-bugs utility such as cat. < 1268077321 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Which is basically the reason WHY they do formal verification nowadays. < 1268077329 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Indeed. < 1268077346 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: For compilers, Reflections on Trusting Trust shows that it is pretty much /unknowable/ whether a compiler is correct. < 1268077365 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Even if the compiler is not malicious, such errors could happen. And verifying that a huge program was compiled correctly? Good luck. < 1268077373 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So we attack the problem at the source, and prove our compiler correct. < 1268077399 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :how does one get a degree sign in LaTeX? < 1268077410 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :in an equation that is < 1268077420 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: If you prove that the generated code is incorrect, you've caught a bug *regardless* of whether it was in the compiler or in the code being compiled. < 1268077434 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION looks at fizzie < 1268077463 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: You don't understand - given a black-box compiler proving that your code was compiled correctly is almost impossible. < 1268077463 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: \circ or something < 1268077464 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Consider: < 1268077473 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: See also http://detexify.kirelabs.org/classify.html < 1268077479 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: ^\circ, I think < 1268077488 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :When we prove the compiler correct, we do it by meticulously analysing every case it uses to compile constructs; we have direct access, we prove the atomic compilations correct, and their compositions. < 1268077491 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant, hm okay < 1268077493 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Voila, the compiler is Always Right. < 1268077495 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :well that works < 1268077498 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268077501 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I think I saw ^\circ used somewhere, yes. < 1268077502 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: If we just have the input, and the output... where do you start? < 1268077503 0 :Deewiant!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: I.e. raise it to the power of one circle :-P < 1268077509 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :You have to model how it was compiled first - basically, write your own compiler. < 1268077512 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Deewiant, hah < 1268077515 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"we do it by meticulously analysing every case it uses to compile constructs" -- *sigh* < 1268077518 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Then you have to verify that each compilation is equal to how your model would compile it. < 1268077530 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: But then we have to verify our now-very-real model compiler is correct, or it's useless. < 1268077534 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: You have the semantics of the program, and you have the semantics of the target language. That's where you start. < 1268077550 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :have you every actually done a formal correctness proof for a non-trivial compiler? < 1268077555 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ever* < 1268077572 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :http://anthony.liekens.net/index.php/LaTeX/DegreesNotation -- that suggests either ^\circ (possibly with your own \newcommand) or the existing \degree from \usepackage{gensymb}. < 1268077580 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Would you prefer I went into the nitty-gritty when the abstarct principles are all that matter here? < 1268077586 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: Me? No. But (as should be obvious) I have reasons for that. < 1268077596 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, not you, alise :p < 1268077596 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: I was thinking ^\circ. Thought it'd be too silly to say. < 1268077612 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :It's less silly than just ^o at the very least. :p < 1268077636 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :fax: For trivial compilers, the problem seems not too difficult, maybe even enjoyable if the compiler is written a certain way < 1268077707 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION needs alise to get into the trenches < 1268077780 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: But my ivory tower is so comfortable... < 1268077796 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Besides, I refuse to do any serious work in anyone ELSE's language. They have cooties. < 1268077818 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1268078091 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Actually (to get back to the previous topic) the problem seems trivial if you construct your compiler compositionally (though I realize full well almost all production compilers aren't, but we were talking about functional languages.) If a->b is correct, and b->c is correct, then a->b->c = a->c is correct. < 1268078129 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :If a->b is correct, and c->d is correct, (a,c)->(b,d) is correct, assuming sane composition < 1268078186 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Now add full-program optimisations. < 1268078204 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Oh yes. The problem AS USUAL is that someone wants it to GO FAST. < 1268078250 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::-D < 1268078446 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1268078457 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :this is not accurate < 1268078510 0 :alise_!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268078545 0 :alise!~d4b78c30@gateway/web/freenode/x-nfmnofcsutzfabmf JOIN :#esoteric < 1268078555 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Mind you, I don't plan on including a clever compiler in my OS. < 1268078566 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :It's near-the-metal, and cpus are really fast. So... < 1268078649 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268078798 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm simply disregarding all considerations of efficiency. < 1268078820 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Waste of time to worry about wasting time. < 1268078840 0 :lament!~lament@S0106001b63f462cc.vc.shawcable.net JOIN :#esoteric < 1268078879 0 :olsner!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: ah, words of truth < 1268078955 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :At the same time, I will continue to complain about web sites that are slow to load. I have a hypocrisy quota to reach, you see. < 1268079060 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://dadgum.com/james/performance.html < 1268079284 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ping < 1268079339 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise: Why are you writing an Othello in Haskell? < 1268079349 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Felt like it. :-) < 1268079683 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Argh! < 1268079684 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I need type-level functions. < 1268079689 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268079701 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :...because I'm implementing a dependently-typed language. :-) < 1268079710 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(But not for /that/ reason.) < 1268079789 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :othello and its rich internal type system... < 1268079825 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :<3 < 1268079843 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ACTION steps back, examines his general structure. < 1268079844 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Happy happy joy joy joy < 1268079854 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Lam :: (Id a -> LC b) -> LC (a :-> b) was so nice, too. Sigh. < 1268079869 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so you Lam-ent its loss? < 1268079872 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :You could even Show it. < 1268079880 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Types: < 1268079893 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :pi (x:T). r < 1268079893 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :* < 1268079903 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I don't believe in ZFC, I don't see why I should believe in dependent types. < 1268079903 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :in pi, T:* < 1268079911 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hehe < 1268079921 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Values: < 1268079926 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ztheist < 1268079928 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :ACTION proves himself < 1268079947 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :\(x:T).(e:R) : pi (x:T). R < 1268079968 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise why don't you write it in Coq (type functions!) then extract it to haskell < 1268079972 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(f : pi (x:T). r) v : r[x=v] < 1268079976 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :if you do that it'll be a really sweet hack < 1268079986 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: mm maybe < 1268080157 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :use monads ! < 1268080223 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :everything's better with monads! < 1268080258 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :sem' xs (App f x) = (sem xs f) (sem xs x) < 1268080260 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :not allowed :( < 1268080267 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :with < 1268080267 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : App :: LC (a –> b) -> LC a -> LC b < 1268080283 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I guess I need to specifically specify f must be a Lam < 1268080297 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :whats xs? < 1268080298 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :how lame < 1268080307 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: de bruijn housekeeping < 1268080322 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :actually I think it needs to be a function... maybe < 1268080334 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :wait, no < 1268080362 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : against inferred type `[(.) (forall a1) (LC a1)]' < 1268080364 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268080365 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(.) < 1268080660 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: sem' :: (Id t -> t) -> LC a -> a < 1268080664 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : sem' v (Var i@(Id n :: Id t)) = v i :: t < 1268080666 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :why doesn't this work :( < 1268080742 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :something to do with needing to enable a bunch of extensions that should really be the default? < 1268080779 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :already done < 1268080785 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : Couldn't match expected type `t' against inferred type `a' < 1268080787 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric ::/ < 1268080816 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :do sem' :: (Id a -> a) -> LC a -> a :D < 1268080817 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :ohh < 1268080818 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I just needed < 1268080822 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :(forall t. Id t -> t) < 1268080823 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :to be the type < 1268080825 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :duh < 1268080830 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :how can that be the right type? < 1268080834 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what's Id t? < 1268080839 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh I see < 1268080867 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :can you implement (in a pure and safe way) STRefs this way? < 1268081023 0 :alise_!~d4b78c30@gateway/web/freenode/x-rbzcgknfpjshhmqa JOIN :#esoteric < 1268081084 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1268081581 0 :oerjan!unknown@unknown.invalid QUIT :Quit: Good night < 1268081647 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :othello is more fun than this < 1268081675 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: I assume there's some hyper-monoidal structure for game boards :-P < 1268081892 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Reifying without _|_: < 1268081893 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :instance (TNat n) => TNat (S n) where reify _ = 1 + ((reify :: (n -> n) -> Integer) id) < 1268081895 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Clever, huh? < 1268081918 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :In fact, you could even have reify :: Dummy n -> Integer where (data Dummy t = Dumb) < 1268081949 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Dummy is basically values indexing on types :P < 1268081985 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Well, sort of < 1268082822 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Press Ctrl-# to continue! < 1268083032 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :wat < 1268083054 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: is there any dependent language that lets you elide most of the obvious proofs and the like... I feel like I'm writing tons of obvious proofs except in haskell atm :) < 1268083078 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :coq < 1268083151 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: you sure? < 1268083166 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well I am interpreting 'elide' in a special way < 1268083306 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that means "specify"? < 1268083395 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah and prove them < 1268083399 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1268083467 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: http://www.reddit.com/r/dependent_types/comments/baf7g/wtypes_good_news_and_bad_news_laquo_epilogue/ why epigram 2 isn't broken < 1268083473 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i think < 1268083504 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :from the murky depths http://sneezy.cs.nott.ac.uk/darcs/RDTP/2ndmeeting/ctm-3.JPG ... < 1268083641 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: btw I think I understood your thing about induction from the logs < 1268083649 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so what is mu-elim's actual type, I'm curious? < 1268083658 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :admittedly this is the rough kind of understanding, not the deep kind < 1268083700 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :huh < 1268083705 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what the heck is going on < 1268083706 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :somehow < 1268083715 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :every X process ended up as STOPPed < 1268083728 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :killall -CONT seems to have helped *somewhat* < 1268083807 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :except I can't resume that dbus crap < 1268083816 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it causes everything else to SIGSTOP again < 1268083821 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Smells like cat food. < 1268083939 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I should really devise a way to isomorph the pure data types with an efficient implementaiton. < 1268083941 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*implementation < 1268083968 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol :D < 1268083996 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what < 1268084019 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I once read a PhD thesis were 70% of the ~200 pages was a transcript of a session with an interactive proof system. < 1268084024 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :*where < 1268084112 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what the hell is going on < 1268084122 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it all started when inkscape crashed < 1268084131 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it seems that resulted in dbus crashing or something < 1268084152 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ooh nice, gconfd is eating 100% CPU < 1268084319 0 :MigoMipo!unknown@unknown.invalid QUIT : < 1268084351 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION snooze < 1268084353 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :No! Sleep! 'Til Brooklyn! < 1268084379 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Formalised proofs are the future! < 1268084384 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Although a transcript is probably not the best form. < 1268084385 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :brb < 1268084402 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :formal math is so difficult < 1268084424 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but it's different than proving stuff on paper, and it's a bit different than programming too < 1268084434 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's a bit perverse < 1268084444 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Can you say "thesis padding"? < 1268084451 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268084916 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm probably going to try to include a proof checker in the language I'm working on. Not a prover though, that's just way too much work. But a proof checker is pretty simple. < 1268084934 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :how do you prevent LaTeX from including a date on the title page? < 1268084996 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :proof checker = type checker < 1268085033 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :proof checker is simple? :) < 1268085037 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yes that is true < 1268085043 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but it is hard to write proofs :P < 1268085045 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric := derivation checker < 1268085070 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Use \date{} -- though it might be suboptimally spaced. < 1268085098 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, hm spacing is important since I don't use a separate title page < 1268085157 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Try it and see. If it's not good, you'll probably have to just do the titles manually; the usual \maketitle is not very customizable. < 1268085170 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :It's possible that it's clever enough to detect and special-case an empty date. < 1268085216 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :someone (fax) gimme the interpretation brackets < 1268085230 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :[[ ]] < 1268085239 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :qwrtuc6ybpoi;ytrweaqstr4jy;poin0[;qwo'm[pn;iqw;p0oi[ie3ye3wdrty;piyuhtw2qwqaretshygu,-';juytdrtuh0poesr48#'[p0oiyhtdryk]=' < 1268085242 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: >:| < 1268085246 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::p < 1268085256 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :hands in the air < 1268085256 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you dirty qwerty user! < 1268085267 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1268085413 0 :Oranjer!~HP_Admini@adsl-71-7-92.cae.bellsouth.net JOIN :#esoteric < 1268085465 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :coq proofs don't look nearly enough like real mathematical proofs < 1268085467 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :imo < 1268085480 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :coq? < 1268085484 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :kazonk; whup f; bop; ligxs < 1268085489 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Oranjer: Coq. < 1268085493 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Theorem prover, programming language. < 1268085499 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :ooh, okay < 1268085583 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise they shouldn't look like what you find in textbooks < 1268085599 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Trivial example of what I have in mind: http://dpaste.com/169655/ < 1268085620 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, well it has been pointed out by Freek that these proof assistants do look very much like Euclids Elements in style < 1268085630 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but I mean on paper stuff is a different world < 1268085644 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah but it shouldn't be a different world! < 1268085655 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :paper can't compute (yet!) :P < 1268085673 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :imo we should all be using dependent formal proofs everywhere < 1268085688 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and with say coq proofs that is .. not practical < 1268085725 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::| < 1268085730 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :more of your bullshit < 1268085751 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :"dependent formal" < 1268085753 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :what < 1268085795 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: you can just not listen to me, you know < 1268085850 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :but ignoring people is the center that all totaltarianism revolves around! < 1268085860 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Dude, we're still grappling with sophisticated SE concepts like "comments" and "tests" < 1268086048 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I am currently trying to add a feature to a swath of our code that another engineer accurately described as an "accretion" < 1268086077 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I would LOVE to be able to prove some simple properties about this code, if only to figure out what the variable names should REALLY be called instead of "ctx" and "data" < 1268086083 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: :-D < 1268086130 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :But it is written in a mainstream programming language, which means, who KNOWS what the semantics of this code REALLY are? How do you even begin to write a proof when your axioms are based on "well, it's implemented this way, on this os, on this cpu" < 1268086133 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :? < 1268086183 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Programming is a shithole/ < 1268086185 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*shithole. < 1268086203 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION gives up on this < 1268086217 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :yay < 1268086224 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION uses a -1.5 em vertical spacer and then violently hits LaTeX with it < 1268086233 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :that seems to work < 1268086294 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it is is an extremely hackish way to get two minipages beside each other. One containing a circuit diagram, the other containing values for components in an eqnarray environment < 1268086295 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :We don't even have debuggers that aren't crap. (Where did this value come from? Tell me. No, you can't, can you.) < 1268086310 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, wonderfully hackish in factr < 1268086313 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fact* < 1268086429 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Indeed. < 1268086443 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I tend to often end up with some negative spaces here and there too, though I always feel I'm doing something wrong. < 1268086445 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Actually you've made me think: perhaps debuggers are isomorphic to proof assistants. < 1268086454 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(Except you never get around to proving anything.) < 1268086472 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: They're certainly related. < 1268086481 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :It's all about tracing. < 1268086561 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :You need to visualize the innards to see why the end result is not what you expected. < 1268086590 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION visualize your innards < 1268086595 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Eww < 1268086610 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :fizzie, actually that wasn't just a negative space. it was a -6 em vertical spacer at the top of a mini page < 1268086620 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :to "fake" it being at level with the other one < 1268086651 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :somehow the display style equation in that mini page caused it to fill out the whole page when it came to vertical placement < 1268086761 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Chrome's search feature is a suckfest ... and not the good kind. < 1268086804 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Howso? < 1268086812 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Just type in what you want and press enter. ...Hooray. < 1268086829 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Or if you're going to search for something that looks like a URL, ?poop://lol. < 1268086839 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I think there's even a shortcut for Ctrl-L + ? < 1268086841 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Nonono, search on a page, its "find" feature < 1268086854 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Whatever you want to call it. < 1268086944 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Oh < 1268086945 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Why? < 1268086998 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :1) What was wrong with '/' and type? 2) The most common use of find on a page for me is getting to a link to click it. But when I hit 'enter', it goes on to the next effing match, it doesn't click the link >_< < 1268087119 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :does it support regex? < 1268087299 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: (1) Oh, Ctrl-F, how horrible. (2) Okay. < 1268087308 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: No. Because it's meant for people to use. Quickly. < 1268087315 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And I can't even fall back to print statements without pulling my hair out because the values have magical stringification so they throw an exception when I try to print them. < 1268087320 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Ctrl is a lot farther from the home row than / is, if searching is common then it's annoying. < 1268087326 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: :-D < 1268087328 0 :tombom!unknown@unknown.invalid QUIT :Quit: Leaving < 1268087338 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :But that's a minor issue, it's the no-click thing that annoys me, surely I don't need to tab to the right link ... < 1268087355 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Chrome is a bit mouse-based. There's an extension that lets you do /foo and the like. < 1268087394 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://github.com/philc/vimium < 1268087467 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, you know, I quite often use egrep as a quick way to search < 1268087475 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: you are not technicaly human though. < 1268087485 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, neither are you if you know any regex < 1268087511 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: Ctrl is *on* the home row. < 1268087525 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Screw you Unixy Solaris keyboard < 1268087540 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, picture < 1268087548 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: I just xmodmap'd. < 1268087559 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :axiom interact : Interaction p f t -> World s -> {p s} -> (t, World (f s)) -- this, but with some sort of way to mark the previous world as invalid < 1268087569 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(I'm trying to formulate all IO as one single interaction axiom.) < 1268087571 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, ah < 1268087577 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, to caps lock? < 1268087586 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Yeah. < 1268087623 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Uniqueness type? < 1268087636 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: Thanks for complicating up my theory :P < 1268087641 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Heheh. < 1268087665 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :basically, (World s) represents a world with conditions s < 1268087684 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(Interaction p f t) is an interaction on worlds; p is Conditions -> Prop < 1268087692 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :meaning "is this interaction acceptable under these conditions?" < 1268087705 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :for instance, a read-from-stream interaction would have a p representing that the buffer must be open in the world < 1268087711 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :f is Conditions -> Conditions < 1268087717 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :representing the effect it has on the conditions of the world < 1268087728 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :a close-stream interaction would require that the stream be open in p, and make it closed in f < 1268087735 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and t is the type of the result it returns < 1268087750 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dependent types would mean that closing an already-closed file would actually be a type error. < 1268087801 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1268087811 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :conor mcbride did some sort of thing on this i know < 1268087841 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and idris < 1268087871 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :heh i'm actualy reading idris stuff now < 1268087875 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1268087877 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :maybe the issue is World < 1268087908 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :dunno < 1268088018 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: how does idris do it? < 1268088107 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :theres papers on it < 1268088121 0 :kar8nga!unknown@unknown.invalid QUIT :Remote host closed the connection < 1268088122 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah but i can't find them < 1268088152 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://www.cs.st-andrews.ac.uk/~eb/drafts/tfp08.pdf < 1268088155 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://www.cs.st-andrews.ac.uk/~eb/drafts/ngna2009-dsl.pdf < 1268088171 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Make a dependent type system where trying to unserialize a corrupt string is a type error! < 1268088300 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Possible but a bit useless since you have to prove it. < 1268088313 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So you'll basically do if corrupt x then fail else yay (long proof) < 1268088326 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Better to have the serialiser return, say, Maybe DeserialisedType < 1268088341 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"Better", sure. < 1268088404 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : dependent types would mean that closing an already-closed file would actually be a type error. <-- anything wrong with that? < 1268088406 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: Just to confirm. http://www.cs.st-andrews.ac.uk/~eb/drafts/tfp08.pdf is not about interaction, yes? < 1268088413 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I skimmed it and didn't see anything related. < 1268088418 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: It's a good thing. Duh. < 1268088427 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, what I thought < 1268088468 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :What about failing to close a file? < 1268088498 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I mean, from a practical perspective, a single guard on "oops, this file handle is already closed" is nothing. But leaking file descriptors is a real problem. < 1268088548 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Actually, yeah, you could. < 1268088565 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Make interact continuation-y and require that the world yielded by the continuation satisfies another bit of the Interaction. < 1268088566 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, also closing a file could fail < 1268088576 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :open-file would have as its ever-ever-postcondition that the file is closed. < 1268088596 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :cpressey, isn't fclose() in C allowed to fail if data is buffered but there is no space to write it? < 1268088621 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Yes, fclose() can fail. < 1268088634 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so, well you could have to propagate some such errors to your high level language < 1268088639 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: i think < 1268088689 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Scylla and Charybdis < 1268088710 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Indeed. < 1268088740 0 :oklokok!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1268088758 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : Scylla and Charybdis <-- ? < 1268088766 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :the latter means "ircd software" to me < 1268088781 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(the one freenode uses nowdays is based on charybdis) < 1268088845 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Gogle it. < 1268088848 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*Google < 1268088871 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, greek mythology? < 1268088885 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No, the other Scylla and Charybdis. < 1268088937 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, [The phrase "between Scylla and Charybdis" has come to mean being in a state where one is between two dangers and moving away from one will cause you to come closer to the other.]? < 1268088987 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :No, the other Scylla and Charybdis. < 1268089018 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, I only get idiom and mythology hits on my first two results pages < 1268089032 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :haven't checked further < 1268089042 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, so what the heck are you talking about < 1268089069 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The other Scylla and Charybdis. < 1268089078 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, there is no such hit for me < 1268089082 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so please explain < 1268089087 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :The other Scylla and Charybdis. < 1268089130 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :okay, now you are just trolling < 1268089200 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's not my fault you're an idiot. < 1268089235 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :for not figuring out you were trolling sooner? perhaps < 1268089259 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I had a hard time imaging you were trolling at first. < 1268089261 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :For convenience, this function may accept either a string, a list, a dictionary, or a file. < 1268089288 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Yes, very convenient. < 1268089313 0 :madbr!~madbrain@modemcable175.136-81-70.mc.videotron.ca JOIN :#esoteric < 1268089336 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Ouch. < 1268089374 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Ever considered just becoming a hermit? < 1268089377 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :A hermit with internet access. < 1268089471 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well yes, if it wasn't for the whole property-tax thing. < 1268089509 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Caves. They have none. < 1268089537 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Then there's that whole evading-park-rangers thing. < 1268089599 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Beats 9-5, right? < 1268089641 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Totally. I should have gone to Hermit School when I had the chance... < 1268089695 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I'm basically banking on becoming a tenured professor because of my sheer genius without trying at some point. < 1268089742 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, then practise backstabbing now, is my advice. < 1268089750 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1268089752 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :You'll need it in grad school. < 1268089829 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Remember when I said sheer genius? < 1268089833 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I'll do it and NOT EVEN REALISE IT. < 1268089843 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Set myself to auto-pilot, baby. < 1268089948 0 :oklokok!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268089952 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ho oklokok < 1268089964 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise tenured how? < 1268089992 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the badass kind that means I can do nothing and never get fired < 1268089997 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :(note: I do not actually believe any of this0 < 1268090003 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*this) < 1268090009 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :like Zeilberger < 1268090061 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :"Academic tenure is primarily intended to guarantee the right to academic freedom: it protects teachers and researchers when they dissent from prevailing opinion, openly disagree with authorities of any sort, or spend time on unfashionable topics" < 1268090073 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :"Zeilberger considers himself an ultrafinitist." Wow, they actually exist?? < 1268090086 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah so I do < 1268090098 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is impressed < 1268090100 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :ultrafinitist? what does that even mean? < 1268090104 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I don't beleive that a^b terminates < 1268090145 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Like other strict finitists, ultrafinitists deny the existence of the infinite set N of natural numbers, on the grounds that it can never be completed. In addition, ultrafinitists are concerned with our own physical restrictions in constructing (even finite) mathematical objects. Thus some ultrafinitists will deny the existence of, for example, the floor of the first Skewes' number, which is a huge number defined using the expone < 1268090146 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :XD < 1268090156 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :It's like argument by lack of imagination < 1268090172 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Argument by well our current computers can't do it/well our current understanding of physics means we can't do it < 1268090175 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Or by vagary in definition of "exists" < 1268090180 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: surely you don't consider yourself such. < 1268090205 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :I can in fact produce an object that is of some arbitrary numerical length. By defining the units appropriately. < 1268090207 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :So ultrafinitists believe there to be a largest number. I wonder what it is :) < 1268090221 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I wonder what it is _today_. < 1268090227 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::-D < 1268090233 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :For instance, I have a meter stick that is roughly G 1/G-meters. < 1268090237 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :yeah that's kooky < 1268090244 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I'm not completely alien to their ideas, but I don't think I am one < 1268090247 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Who pinged me? < 1268090264 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :alise_: the largest number is 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875897 < 1268090277 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lament: 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875898 < 1268090279 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :lament: 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875898 < 1268090282 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Suck it. < 1268090283 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :haha < 1268090290 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :that's not a number < 1268090295 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :just a meaningless string of digits < 1268090301 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh lament is a 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875897-finitist < 1268090302 0 :Oranjer!unknown@unknown.invalid PRIVMSG #esoteric :it is a number < 1268090309 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :you could argue that numbers larger than X don't have any practical use, that's kinda dumb < 1268090313 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :It's the successor of the largest number you proclaimed. < 1268090316 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :it doesn't mean anything. Numbers can't be that large. < 1268090319 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :it's not a number < 1268090327 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :lament: Define number. < 1268090330 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :no u < 1268090332 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm a 2^16-finitist < 1268090356 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: lament thinks such a finitism doesn't exist < 1268090357 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :so there < 1268090357 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :data Number = Zero | Succ Number < 1268090388 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, fix Succ -- where is your arithmetic now? < 1268090391 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :math isn't haskell < 1268090395 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Nat := Mu (Unit &) < 1268090398 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lament, ask #haskell :x < 1268090409 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Succ it. < 1268090409 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :why? I'm more qualified than #haskell < 1268090412 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :fax: Congrats, you just defined infinity. < 1268090415 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why doesn't oklocorpse talk to me :( < 1268090417 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :i've a math degree, most people in #haskell don't. < 1268090421 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok oklokok oklokok < 1268090424 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: ugh, no < 1268090433 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :_|_Nat is not infinity < 1268090459 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Fine, fine. He's defined _|_ :: Number. < 1268090470 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lament: hey did you specialize? < 1268090475 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :at some point < 1268090476 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :no < 1268090478 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric : why doesn't oklocorpse talk to me :( <-- I guess he got tried of saying BRAAAINS? < 1268090547 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lament :( < 1268090573 0 :oklokok!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1268090625 0 :oklokok!~oklopol@a91-153-117-208.elisa-laajakaista.fi JOIN :#esoteric < 1268090640 0 :madbr!unknown@unknown.invalid PRIVMSG #esoteric :damn postmodernists < 1268090650 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :postpostmodernism < 1268090739 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok? < 1268090760 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :ω exists because I can describe it (I can describe Atlantis too) < 1268091008 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ω is shorthand for some definition in some system of axioms. in those, it is presumably a coherent concept < 1268091022 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the problem is that you want Atlantis to be a concept of this world. and we don't control /our/ axioms. < 1268091048 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :God no, I don't want that. They would cream us with their nuclear laser missiles! < 1268091065 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1268091081 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ACTION sighs there are so many things I want to do that I am unable to do any of them < 1268091102 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I love how the Halting Problem is equivalent to the Entscheidungsproblem. < 1268091124 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah that's a good one < 1268091226 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :meeee < 1268091228 0 :lament!unknown@unknown.invalid PRIVMSG #esoteric :s/things/women < 1268091267 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :decide : (∀a. Prog a → Bool) → (P : Prog (Nat → Bool)) → Bool < 1268091268 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :decide H P = ¬(H 《i := 0. Do: If ¬(P i), break. i := i + 1. Loop. 》) < 1268091275 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Or thereabouts. < 1268091355 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi oklookpaoufpadda < 1268091362 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I got something to show you < 1268091374 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :www.stanford.edu/~dgleich/publications/finite-calculus.pdf ! < 1268091384 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you said you didn't like analysis because it wasn't finite enough < 1268091489 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :well i'm not sure that's exactly that i said :D < 1268091492 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :but i'll check < 1268091492 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :http://i43.tinypic.com/2v8s9w8.png < 1268091495 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :whoope < 1268091496 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I see fax doesn't like my proof :( < 1268091499 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok this stuff is so cool though! < 1268091500 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :Scientist: Yeah, the expansion of the universe is accelerating and there seems to be stuff that seems to to exert negative gravity and that stuff is dark energy < 1268091502 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :seriously I have to master it < 1268091503 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :Dude: and what is that, what is it made of? < 1268091504 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :sorry spam < 1268091506 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :Scientist: Really we have no fucking clue, we hoped you'd stop asking after hearing "dark energy" < 1268091510 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :bye < 1268091515 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise: I just assumed it was correct < 1268091519 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Wareya: yawn < 1268091532 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yet another lol-they-call-it-dark-it-must-just-be-made-up bullshit story < 1268091539 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :be ignorant elsewhere :| < 1268091575 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :decide on the reals is interesting btw < 1268091576 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :who said I agree? < 1268091579 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :it's just funny < 1268091579 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :nested halting-checking < 1268091580 0 :Wareya!unknown@unknown.invalid PRIVMSG #esoteric :byer < 1268091609 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :I can describe black holes < 1268091647 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :[Note to the editor: Insert a "your mom" joke here.] < 1268091651 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :[No. -Ed] < 1268091741 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, that's what she said! < 1268091745 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :night → < 1268091989 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://en.wikipedia.org/wiki/Clifford_Stoll The acme klein bottle guy is also the caught Markus Hess guy and also thought interwebs would never catch on < 1268092234 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopkoupuo i think this is a precursor to Umbral Calculus < 1268092252 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :not entirely sure < 1268092391 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok btw I have not done OR yet :( < 1268092408 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :actually I was going to try and code that stuff into epigram just for fun but it was too hard < 1268092423 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(I couldn't even define a tree type) < 1268092434 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_, what did you think of my proof? < 1268092438 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :you can ask for hints if you want < 1268092455 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: which proof? < 1268092456 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok, well if you had an intermediate problem between AND and OR that would be good :p < 1268092468 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :http://dpaste.com/169655/ < 1268092488 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :It's wrong. The last thing on the 3rd line should be "Stack'" < 1268092505 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: You've neglected to specify what you're proving, for starters. < 1268092518 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Looks more like an evaluation to me, < 1268092519 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*me. < 1268092543 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Theorem is always: first line and last line of "proof" section are equal. < 1268092546 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :well the thing is < 1268092555 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: That's a rubbish proof system < 1268092556 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :What is a proof if not an evaluation? < 1268092556 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :Gian-Carlo Rota began his career as a functional analyst, but changed directions and became a distinguished combinatorialist. -- he helped develop this umbral calculus < 1268092559 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :for most things that are in the middle, you'll need to have OR already < 1268092562 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: A proof is a value < 1268092562 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :i mean most things i know < 1268092578 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: link to that book that had tons of proofs in i think coq < 1268092578 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :Well, sure, everything is a value < 1268092578 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :if you can live with using OR before knowing how to compile it, then yeah i have a few < 1268092581 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :supposedly from the future < 1268092587 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: No, quite literally < 1268092594 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :p : P where P : Prop = p is a proof of P < 1268092621 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok oh, I was thinking about AxB = BxA, it seems to only have solutions like A = (mnux)^n(mnu), B = ..^m... < 1268092622 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :there's a reason proof assistants are all dependent and whatnot, it's because this is the way things make sense in computing < 1268092647 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise, I don't know what you are referring to < 1268092658 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :not all proof assistants work on dependent type theory < 1268092673 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but dependent type theory is really an excellent way to do it imo < 1268092693 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :if |A|>|B|, then TxB = xBT, which gives you all the solutions < 1268092703 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: well yeah < 1268092711 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklokok huh?? < 1268092713 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :there are a few basic techniques that get you through most things < 1268092717 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :not all-are dependent < 1268092721 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :but are all-dependent-and-whatnot < 1268092730 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :fax: i just substituted A = BT because |A| > |B| < 1268092739 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :there's a symmetric case for B > A < 1268092745 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1268092752 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ah! < 1268092757 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :oh and after that you already have all the solutions < 1268092765 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :if you don't see it... see fundamental theorem < 1268092769 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :;) < 1268092775 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :alise_: To be clear, it's not a proof finder, it's only a way to write out proofs so that they can be checked. < 1268092783 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :cpressey: Of course. < 1268092786 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :we should probably be doing this in pm, i'm not sure it's as entertaining to others < 1268092789 0 :cpressey!unknown@unknown.invalid PRIVMSG #esoteric :And since a proof is a series of derivations, I don't see anything wrong with this. < 1268092794 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :well actually < 1268092799 0 :oklokok!unknown@unknown.invalid PRIVMSG #esoteric :we should be doing this tomorrow