00:00:04 <MissPiggy> 1::2::3::nil is represented as <3, {yes->1;no->2;maybe->3}>
00:00:24 <MissPiggy> r::q::p::::snil is represented as <4, {north->1;south->2;east->3;west->4}>
00:00:35 <MissPiggy> r::q::p::s::nil is represented as <4, {north->r;south->q;east->p;west->s}>
00:00:48 <alise_> ok, so what's the induction for T'?
00:01:03 <MissPiggy> ill tell you if you get it right :)
00:02:27 <alise_> Ordinarily I'd love to, but - I really should have left many minutes ago.
00:02:49 <alise_> 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.
00:02:57 <alise_> Or you could wait for both. Your choice.
00:05:14 <MissPiggy> there is no way you can possibly understand the scheme for Muu
00:05:35 <alise_> But I'm interested in it regardless.
00:05:47 <MissPiggy> it will be very simple and clear once if you just approach it step by step
00:06:25 <alise_> Yes, but I /really really/ have to go. Surely, there is no harm in telling me it?
00:06:35 <MissPiggy> well I don't know how to write it out either
00:06:47 <MissPiggy> we need to establish some new notation together first
00:07:05 <alise_> just use any existing language :P
00:07:09 <alise_> or are they not appropriate?
00:07:31 <MissPiggy> P(L') -> (forall n, forall f, (forall i, P(f i)) -> P(B' f)) -> forall t', P(t')
00:07:38 <MissPiggy> that's the scheme for T' I wish you had got it
00:08:03 <alise_> i probably would have if i tried
00:08:08 <alise_> but /i/ /have/ /to/ /go/
00:08:11 <alise_> please try and understand
00:08:17 <MissPiggy> so for T, P(L) -> (forall l, [] P l -> P(B l)) -> forall t, P(t)
00:08:28 <MissPiggy> [] is a new notation we have invented
00:08:43 <MissPiggy> [] P (a::b::c::d::nil) = P a /\ P b /\ P c /\ P d
00:09:09 <MissPiggy> [] is defined for any strictly positive functor
00:09:20 <MissPiggy> (proof of this is in some paper I can show you later)
00:09:27 <MissPiggy> this is enough to define induction on Mu
00:11:07 <Sgeo> It's the end of days for There.
00:12:17 <Sgeo> "DSL/Cable modem: 25 minutes"
00:12:23 <Sgeo> for a 47MB download
00:12:44 -!- alise_ has quit (Ping timeout: 252 seconds).
00:17:37 -!- FireFly has quit (Remote host closed the connection).
00:22:37 -!- coppro has joined.
00:32:03 -!- BeholdMyGlory has quit (Remote host closed the connection).
00:48:18 * Sgeo wants to play on FICS against someone he knows
01:01:47 * pikhq has been futzing a tiny bit with TinyGC...
01:01:59 <pikhq> ... It appears to work, and appears to be slow.
01:02:42 <coppro> Sgeo: what's your rating?
01:03:03 <Sgeo> coppro, um, it's been years since I was last on FICS
01:03:05 <Sgeo> How do I get that?
01:03:29 <coppro> I just didn't want to play against someone way better than me
01:03:31 <Sgeo> Um, rating for Blitz or Standard or Lightning?
01:03:40 <Sgeo> coppro, I'm probably not better than you
01:03:45 <Sgeo> It's been years since I played chess
01:06:23 <coppro> Sgeo: what time controls do you want?
01:06:55 <Sgeo> Regular, I guess
01:07:37 <coppro> Sgeo: it says you're examining a game
01:12:14 * Sgeo clearly has no clue what he's doing
01:12:56 <coppro> I only have a little more than you
01:13:15 <coppro> I can give you some pointers afterward, if you'd like
01:17:06 -!- MissPiggy has quit (Quit: Lost terminal).
01:17:18 * Sgeo isn't really thinking anything through that much
01:20:21 <coppro> You went downhill around move 16
01:30:26 <Sgeo> I've lost, haven't I?
01:34:21 <Sgeo> [In case anyone cares, I just lost]
01:34:26 <Sgeo> coppro, what client do you use?
01:34:45 <coppro> it's not great, but it's not terrible
01:34:46 * Sgeo is using BabasChess
01:34:54 <Sgeo> Used to use Chess Machine and love it
01:37:22 -!- lament has quit (*.net *.split).
01:37:22 -!- HackEgo has quit (*.net *.split).
01:38:45 -!- lament has joined.
01:39:59 -!- HackEgo has joined.
01:44:13 <Gregor> bsmntbombdood: OK, I'm putting that on sibeli.us for the moment.
02:08:55 <Sgeo> Anyone want to see the game between coppro and I?
02:10:35 <Gregor> I am so suck at chess.
02:17:45 <Sgeo> Gregor, bet you're better than me
02:17:54 <Sgeo> I haven't played in YEARS
02:18:00 <Sgeo> And when I had, I barely paid attention
02:18:36 <Sgeo> I know the mechanics, just no strategy
02:18:52 <coppro> Sgoe: you were pretty good for the first half
02:18:57 <coppro> but then your moves just became random
02:19:15 <coppro> although you missed some opportunities to develop; getting pieces out and involved is key
02:20:34 -!- oerjan has joined.
02:22:46 <oerjan> <AnMaster> hm... FAUST "Functional AUdio STream"... What are the chances of that name NOT being designed to fit the acronym?
02:23:12 <oerjan> exceedingly tiny i'd say, since if they didn't know about faust, FAST would have been closer
02:23:42 -!- coppro has quit (Quit: I am leaving. You are about to explode.).
02:24:10 -!- coppro has joined.
02:26:54 -!- gm|lap has joined.
03:02:04 <Gregor> oerjan: Awesome catch :P
03:02:53 <Gregor> 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.
03:07:13 <Sgeo> http://ficsgames.com/cgi-bin/show.cgi?ID=243952855;action=show
03:09:39 -!- adu has joined.
03:10:22 -!- Asztal has quit (Ping timeout: 264 seconds).
03:36:18 -!- oerjan has quit (Quit: leaving).
03:38:57 -!- gm|lap has quit (Quit: HydraIRC is a child molester -> http://silverex.net/news <- i couldn't change my quit message).
03:39:09 -!- GreaseMonkey has joined.
03:43:57 <pikhq> GreaseMonkey: Generic Music Idol Band Star Game?
03:44:02 <pikhq> Gregor: Generic Music Idol Band Star Game?
03:44:17 <pikhq> Clearly, something *that* generic should have the sequence generated from the sheet music!
03:44:36 <Gregor> Impossible, the recording, being of non-shitty music, doesn't have a constant tempo.
03:44:40 <pikhq> ... And by sheet music, I mean a convenient, easy-to-parse subset!
03:45:25 * pikhq tries to think of non-shitty music with a constant tempo...
03:45:30 * pikhq is having severe difficulty.
03:46:13 <pikhq> Okay, I'm having trouble thinking of *shitty* music with a constant tempo now. :P
04:00:51 <Gregor> Oh, I never really answered your question.
04:01:20 <Gregor> Generic Music Idol Band Star Game is a generalization of DDR, Guitar Hero, Rock Band, and all the other identically dull games out there.
04:01:58 <Gregor> Currently it's roughly equivalent to DDR, for the others I would need non-instant events, but that's a trivial addition really.
04:02:19 <Gregor> And of course the horrendous karaoke part that should earn the death sentence to all who play it is excluded.
04:05:21 <pikhq> Hey, DDR started it and was unique...
04:05:31 <pikhq> ... And then came more bemani from Konami...
04:05:34 <Gregor> And it was not unique.
04:05:39 <Gregor> Parappa the Rapper started it.
04:05:54 <Gregor> DDR merely introduced a non-gamepad controller to the equation.
04:05:59 <pikhq> ... And then they started releasing games with just the music changed...
04:06:24 <pikhq> And then Guitar Hero and Rock Band came around.
04:06:43 <pikhq> Well after the genre had been beaten into a bloody, homogenous pulp.
04:07:28 <Gregor> 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.
04:07:53 <Gregor> 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.
04:07:54 <pikhq> DDR's the home version of an arcade game.
04:08:32 <Gregor> Well fine, they were the first ones clever enough to devise an alternate control mechanism, which they used initially in arcade :P
04:09:06 <Gregor> 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.
04:09:40 <Gregor> But it's also an amusing thing to parody with Finlandia :P
04:09:44 <pikhq> DDR is quite enjoyable. But... Yeah, the whole genre is ridiculously repetitive.
04:09:57 <pikhq> "Oooh, let's make a new game, but with *different songs*!"
04:10:01 <Gregor> Also, http://upload.wikimedia.org/wikipedia/en/4/4f/Inch_converter.jpg is the most horrifying thing I've ever seen.
04:10:16 <pikhq> "Hey, I got something better! Let's change the brand name and *have a different controller*!"
04:11:08 <pikhq> And of course, no useful skill involved. Just a useless one.
04:13:18 <Gregor> 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.
04:13:32 <Gregor> Actually, hahahah, y'know what really started the genre?
04:13:36 <Gregor> Miracle Piano Teaching System
04:13:51 <pikhq> Also of note: DDR functions as a form of exercise. Everything else... Is about as useful as playing air guitar.
04:14:45 <Gregor> 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.
04:15:50 <pikhq> 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.
04:16:04 <pikhq> And that is why all males do anything, right? :P
04:17:05 <Gregor> It's worked out well for me! >_>
04:18:08 <pikhq> The karaoke-thing on Rock Band, tangentially, is damn near impossible if you can sing.
04:18:31 <Gregor> You're not allowed to use vibrato, yes?
04:18:41 <Gregor> Or rather, you'll be penalized for it.
04:18:44 <pikhq> Or... Anything else.
04:18:59 <pikhq> And God help you if you're not used to singing the melody. :P
04:19:20 <Gregor> This is Rock BAND, not Rock CHOIR
04:19:51 <Gregor> Although a choral GMIBSG would be ... impossible for the neanderthals that play that kind of game to figure out *shrugs*
04:19:56 <Gregor> Feh, that was offensive.
04:20:03 <Gregor> Neanderthals aren't so bad, really.
04:20:31 <Gregor> Let's say ... australopithecus.
04:20:38 <pikhq> Eh, most people play it as an excuse to be with friends.
04:20:46 <pikhq> Kinda silly to need an excuse, but hey.
04:21:07 <Gregor> I MIGHT have negative opinions about this genre of game :P
04:21:45 <pikhq> I have negative opinions about most of the genre simply because it's been beaten in the ground more than even freaking sports games.
04:22:44 <pikhq> Oh, and the choice of music for them usually *sucks*.
04:23:06 <Gregor> Of course, they need the most constant and dull music possible to make the game possible.
04:23:16 <Gregor> Aside from the fact that if it was good, royalties would be too expensive.
04:23:38 <pikhq> DDR tends to commission music.
04:23:51 <pikhq> And Guitar Hero commissions... Covers.
04:24:02 <pikhq> Very annoyingly poor covers, too.
04:24:14 <Gregor> The whole concept of covers amuses me a lot, btw.
04:24:34 <pikhq> It is kind of amusing, yes.
04:24:36 <Gregor> I want to convince my cellist friend to say he's doing a cover of Shostakovich some time :P
04:25:16 <pikhq> All because of the singer-songwriter thing that started getting common in the 50s...
04:26:12 * pikhq got reminded of that terrible Kansas cover again.
04:26:17 <Gregor> 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.
04:26:39 <pikhq> Gregor: The majority of *popular* ones, perhaps.
04:26:48 <Gregor> Naturally that's what I'm referring to, yes.
04:26:58 <Gregor> The popular singer-songwriters today aren't even singers. They're boobs with autotuners.
04:26:59 <pikhq> When you get outside the realm of popular musical shovelware, then you start seeing talent.
04:27:25 <pikhq> Heck, just get outside the past couple decades or so and you start seeing talented people that are popular.
04:27:50 <Gregor> So, you're saying that music continues its steady slide into the abyss :P
04:27:51 <pikhq> Freaking autotune.
04:28:11 -!- Oranjer has joined.
04:28:20 <pikhq> Nah, just the stuff that gets shoved down people's throats that I'm not sure how anybody can like.
04:28:39 <Gregor> Awesome timing for Oranjer to waltz in :P
04:29:09 <Oranjer> I'm guessing it's...religion?
04:29:32 <Gregor> Not particularly close.
04:29:35 <Gregor> Could be farther though.
04:29:48 <Gregor> There are logs, y'know :P
04:29:53 <pikhq> Music. Specifically, manufactured music produced by the RIAA.
04:30:23 <pikhq> Examples include Celine Dion and Nickleback.
04:30:35 <Oranjer> Celine Dion is a national treasure
04:30:50 <Gregor> Boobs with an autotuner.
04:31:04 <Oranjer> boobs with an autotuner is a national treasure
04:31:13 <Gregor> Y'know, if they built the autotuner right into the breast implants, they could save a lot of trouble.
04:32:10 <Oranjer> in soviet russia, blah blah...
04:32:57 <GreaseMonkey> http://pubacc.wilcox-tech.com/~greaser/mods/dootman.it if you're lacking somewhat interesting music
04:33:04 <pikhq> You want a national treasure? *Jimi Hendrix* is a national treasure.
04:42:07 <augur> jimi hendrix is dead.
04:42:14 <augur> he can't be a national treasure.
04:42:25 <pikhq> augur: WE WORSHIP HIS BONES.
04:42:34 <Oranjer> his bones have gone missing
04:42:43 <Oranjer> we have to go on a quest to find them
04:42:46 <augur> well, ofcourse his bones have gone missing
04:42:54 <augur> he's been resurrected
04:44:21 <Oranjer> National Treasure 3: Zombie Hendrix would be, literally, the best movie conceivable
04:45:21 <Gregor> There were some movies called "National Treasure", weren't there?
04:45:38 <Gregor> Clearly not movies I ever saw :P
04:49:47 <pikhq> They weren't... Notable.
04:52:37 <Sgeo> o.O at coppro's record on ficsgames.com
04:52:42 <Sgeo> Although it's better than mine
04:53:41 <Oranjer> the first info I see on that site is entirely opaque
04:54:30 <Sgeo> Free Internet Chess Server [ freechess.org ]
04:54:30 <Oranjer> does this handle variants?
04:55:05 <Gregor> 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"
04:55:08 <Oranjer> which means you can't define your own
04:55:22 <Oranjer> well, that's my first thought with anything ever, so yay!
04:55:26 <Gregor> (OK, not thousands ;) )
04:56:06 <Sgeo> Well, there's some ability to define your own starting positions I think
04:56:25 <coppro> Sgeo: don't look there :P
04:58:33 <pikhq> It'd be nice if it did shogi...
04:59:04 <Oranjer> isn't there a program out there that lets you play any chess variant?
04:59:11 <Oranjer> including chess and go, I think
04:59:15 <Oranjer> 1,000...something, I think
04:59:57 <pikhq> Gregor: Shogi is a chess-family game.
05:00:29 <Oranjer> damn, I finally found the program
05:00:47 <Oranjer> http://www.zillions-of-games.com/
05:00:59 <Gregor> pikhq: I was being intentionally stupid :P
05:01:22 <Oranjer> http://www.chessvariants.org/programs.dir/zillions/
05:01:26 -!- Gracenotes has joined.
05:09:22 * Sgeo should probably do something that will give him nutrition
05:24:03 <coppro> FICS has a number of popular variants, but nothing like new pieces
05:24:43 <Gregor> I reluctantly admit, after much time using Firefox, that Chrome is a far more reliable browser >_>
05:24:52 <coppro> The client-server model makes that difficult
05:25:03 <coppro> yeah, Firefox gets major slops for reliability
05:25:12 <Gregor> 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?
05:26:13 <Oranjer> that question seems obvious to me--but I fear that in asking it, you suggest a deeper answer?
05:27:16 <pikhq> Gregor: When Flash stalls in Firefox, Firefox shits itself.
05:27:26 <pikhq> When Flash stalls in Chrome, Chrome kills the process.
05:27:49 <Gregor> I'm not referring to halting or crashing, just momentary stalls.
05:28:16 <pikhq> That's just because Firefox's implementation of the NSAPI sucks.
05:28:18 <Gregor> e.g. Hulu plays seamlessly in Chrome, but is gappy and shitty in Firefox.
05:29:32 * pikhq tries installing Chromiumn
05:34:40 <Gregor> I just trust Google's intentions less and less recently ...
05:34:59 <Oranjer> shh! don't let them hear you!
05:35:32 <Sgeo> You can always download SRWare Iron
05:35:54 -!- oklokok has quit (Ping timeout: 248 seconds).
05:42:36 <pikhq> Gregor: Chromium is probably in your package manager.
05:43:04 <Gregor> That would be how I installed it.
05:43:15 <pikhq> Why that's not Chrome.
05:43:19 <pikhq> Has none of the nasty bits.
05:43:45 <Gregor> I thought Chromium was the devel name
05:44:33 -!- oklokok has joined.
05:54:26 -!- oklokok has quit (Ping timeout: 265 seconds).
06:05:52 -!- oklokok has joined.
06:14:49 <pikhq> Chrome takes ages to compile.
06:20:20 <Gregor> g++ chrome.cc -lages -o chrome
06:25:30 * Gregor 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"
06:29:04 <pikhq> Now I'm waiting on the code going into /usr/src/debug. Hooray.
06:29:25 <pikhq> (... So I like the ability to use gdb when something segfaults...)
06:34:53 -!- sebbu2 has quit (Ping timeout: 260 seconds).
06:34:54 -!- sebbu has joined.
06:40:37 -!- MizardX has quit (Read error: Connection reset by peer).
06:46:32 <Sgeo> How does http://www.geocities.com/lifemasteraj/beginner1.html still exist?
06:47:50 <Sgeo> What universe do these people come from? http://www.mywot.com/en/scorecard/geocities.com
06:48:04 <Oranjer> Sgeo, this is mind boggling
06:48:23 <Sgeo> The WOT stuff, or the continued presense of the geocities site>
06:52:17 <Gregor> Good lord, it's so Geocities too X-D
06:53:32 <Sgeo> Maybe e's paying for hosting?
07:04:29 -!- tombom has joined.
07:10:14 -!- Oranjer has left (?).
07:48:44 -!- tombom has quit (Quit: Leaving).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:16:24 -!- GreaseMonkey has quit (Quit: HydraIRC -> http://www.hydrairc.org <- Nobody cares enough to cybersquat it).
08:38:17 -!- cmeme has quit (Ping timeout: 265 seconds).
08:46:13 -!- sebbu has quit (Ping timeout: 258 seconds).
08:47:21 -!- cheater2 has quit (Ping timeout: 248 seconds).
08:48:33 -!- cheater2 has joined.
08:50:28 -!- sebbu has joined.
08:57:50 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
09:11:25 -!- adu has quit (Quit: adu).
09:50:53 -!- FireFly has joined.
09:52:09 -!- ais523 has joined.
10:17:15 -!- MizardX has joined.
10:41:01 -!- ais523 has quit (Remote host closed the connection).
10:50:25 -!- ais523 has joined.
12:26:30 -!- BeholdMyGlory has joined.
12:30:07 -!- alise has joined.
12:30:10 <alise> 16:08:17 <MissPiggy> so for T, P(L) -> (forall l, [] P l -> P(B l)) -> forall t, P(t)
12:30:16 <alise> sorry, had already left at that point
12:32:28 <alise> I'll play anyone at chess! Extremely badly!
12:35:06 <ais523> alise: hmm, I used to be OK at chess, but haven't practiced in years
12:35:22 <ais523> major issue for me would be finding a chessboard that doesn't automatically suggest moves for me
12:35:33 <alise> I've been beaten by a non-prodigy twelve year old.
12:35:54 <ais523> tell you what, I think my really awful chess AI still runs in DOSBox
12:36:06 <alise> ais523: there are billions of clients for FICS
12:36:14 <alise> Sgeo and coppro played yesterday, see logs for what clients they used
12:36:37 <ais523> oh, I just assumed each player would use their own board and you'd send moves over IRC
12:38:10 -!- MigoMipo has joined.
12:38:17 <alise> ah; i have no chessboard at all here
12:38:30 <ais523> ugh, it seems that although it runs in DOSbox, it captures both the keyboard and mouse
12:38:42 <alise> and, also, I'm so bad it'd take me ages to figure out how to express the moves I make :-)
12:38:44 <ais523> thus making it impossible to switch windows, or otherwise communicate with people
12:38:45 <alise> maybe I could use a program and you could use a real board
12:38:59 <ais523> alise: I meant, setting something like GNU chess to 2-player mode to use it as a board
12:39:17 <alise> or we could just sign up for fics :P
12:39:34 <alise> and have my horrible failure recorded for all eternity
12:39:46 <ais523> hmm, almost works in wineconsole
12:39:54 <ais523> only issue is that it sizes the screen incorrectly
12:40:10 <ais523> <wineconsole> fixme:int:DOSVM_Int10Handler Load ROM 8x8 Double Dot Patterns - Not Supported
12:40:35 <ais523> hmm, and that one shouldn't even be hard, you can simply implement it by doubling the vertical height of the screen
12:40:44 <ais523> (virtual screen, that is)
12:40:46 <alise> in fact, i'm sure someone must have made a java applet client for fics
12:40:57 <alise> yeah but wine is shit :P
12:41:14 <alise> let's get crysis 5 working! who cares about the rest of the api
12:41:29 <alise> we want to support the gaymen community :|
12:41:38 <ais523> meh, running a program and only 2 fixmes, that's not bad
12:41:51 <ais523> besides, I've run stuff in WINE that I really needed to be able to run in order to get projects done
12:42:13 <ais523> it works just fine on MPLAB C30, except that it makes MPLAB spout a few warnings when it loads
12:48:47 <alise> ais523: fics or manual? I have the fics regpage up here
12:49:05 <ais523> manual, because playing games over a work connection is hard to explain
12:49:33 <ais523> but I'm assuming attempting to keep track of everything said on IRC would be a fool's errand
12:50:26 <alise> you're disrupting one of my essential tactics! (decide what to do instinctively so that every move takes about a second) :-P
12:50:29 <Deewiant> Or did you mean the lack of even a local chessboard
12:50:52 <alise> ais523: also, the irc bytes sent and the chess bytes sent will be pretty much identical, you know
12:50:59 <alise> in fact, the chess bytes may be binary and thus more obscure
12:51:15 <ais523> alise: the chess bytes will have headers
12:51:28 <ais523> and won't go through at all if they're on a nonstandard port
12:51:34 <ais523> you can automatically see where the bytes are sent
12:52:15 * alise googles for chess over irc out of curiosity; maybe there's something that'll automate it for me
12:52:42 <Deewiant> Don't know about other clients
12:52:57 <Deewiant> (And I haven't tried the irssi one either, I just know about it)
12:53:56 <alise> yeah i saw that but i meant a chessboard program that actually sends and recvs the moves itself
13:02:27 -!- oerjan has joined.
13:03:20 <alise> Deewiant: I can't decide whether you'd be better or worse than ais523
13:03:52 <ais523> well, I have no idea how good Deewiant is at chess; I'm formerly-decent-but-out-of-practice
13:04:03 <ais523> maybe in the top 2 or 3 in the school while I was at secondary school
13:04:08 <alise> I'm rather surprised how little this stock Windows 7 is annoying me
13:04:24 <Deewiant> I'm formerly-not-entirely-shit-but-out-of-practice
13:04:28 <alise> I mean, sure, it sucks, but..
13:04:38 <alise> Load, you fucking downloa page!
13:04:38 <ais523> IE8 is so much better than IE6, that's why it feels so good
13:04:42 <alise> I want my chess client.
13:04:52 <alise> ais523: I know, but I keep forgetting I'm actually using IE as opposed to, say, Firefox
13:05:26 <alise> and I actually really like using the taskbar to switch tab
13:05:27 <ais523> without extensions, there aren't many user-visible differences between even IE7 and Firefox
13:05:39 <ais523> also, taskbar to switch tabs would be a nightmare the way I use tabs
13:06:18 <alise> but the thing is, I use alt-tab to switch windows mostly
13:06:22 <alise> so it's actually quite nice
13:07:10 * alise tries to figure out how to get winboard to do two-player
13:07:34 <Deewiant> 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
13:08:21 <Deewiant> Probably all the active chess club people there (maybe 10-20 of them?) could beat me without too much trouble
13:08:37 <alise> This seems to not do two-player offline. Sigh.
13:08:57 <ais523> you could probably have written a chess client yourself by now
13:09:11 <alise> Deewiant: ais523 refuses to because of work connection
13:09:15 <ais523> I used to write them for practice when I was younger; I think I wrote one in Excel
13:09:19 <alise> also it does, but only one-player-against-engine
13:09:20 -!- Asztal has joined.
13:09:27 <Deewiant> alise: Yes, but if you want to play me instead ;-)
13:09:36 <Deewiant> alise: And no, there's mode -> edit game
13:09:43 <alise> ais523: Last chance before I cruelly cast you aside in favour of a real man
13:09:48 <Deewiant> Which is basically equivalent to two-player one-machine
13:09:56 <ais523> alise: last chance to what?
13:10:01 <Deewiant> Except that it doesn't have timing
13:10:02 <ais523> I don't mind not playing if it's too hard to set up
13:10:16 <ais523> Deewiant: "edit game", what a ridiculous name for it!
13:10:20 <alise> Well, use FICS or I cast you aside for now :P
13:10:30 <Deewiant> ais523: Well, it's not really a two-player mode.
13:10:54 <alise> Deewiant: do I need to register for fickz?
13:10:55 <Deewiant> 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.
13:11:05 <Deewiant> alise: I don't know how it works. :-P
13:11:11 <alise> That could make future moves impossible, surely?
13:11:28 <Deewiant> Well, surely it deletes the history from that point forward.
13:11:32 <alise> If you are not a registered player, enter guest or a unique ID.
13:11:55 <alise> "alise" is not a registered name. You may use this name to play unrated games.
13:11:59 <alise> Deewiant: Well, connect.
13:12:08 <Deewiant> I am connected, I even registered.
13:12:19 <ais523> could we have the moves posted in-channel somewhere so I can watch?
13:12:27 <ais523> maybe not this channel, though
13:12:44 <alise> #deewiant-alise-champ-2010
13:18:41 -!- alise_ has joined.
13:20:42 -!- alise has quit (Ping timeout: 252 seconds).
13:28:33 -!- oerjan has quit (Quit: leaving).
13:50:02 -!- alise_ has quit (Ping timeout: 252 seconds).
15:01:58 -!- cpressey has joined.
15:41:33 -!- alise has joined.
15:41:55 <alise> Name for a Reversi-playing program: Infersi
15:43:52 -!- coppro has quit (Quit: I am leaving. You are about to explode.).
15:44:25 <ais523> coppro's quit message has been false every time so far
15:44:32 <ais523> I'm starting to suspect he doesn't actually mean it
15:44:44 <ais523> either that, or it isn't targeted at me, in which case some context would be helpful
15:45:17 <alise> I've exploded several times when he's left
15:47:37 <alise> I wonder what the most practical Haskelly thing is for making a GUI
15:47:57 <ais523> I have no idea, but deep-down I hope it indirectly involves Befunge
15:49:01 <Deewiant> Write Befunge code that uses WIND and then system "rcfunge tmp.b98" ?
15:49:44 <ais523> something like that, but with more tight binding on the Haskell
15:49:51 <ais523> maybe you could go via INTERCAL
15:49:51 <alise> Also, that's Windows-only
15:50:04 <ais523> if INTERCAL doesn't have Haskell bindings yet, it probably should do
15:50:21 <ais523> mostly to annoy Haskell advocates
15:50:32 <Deewiant> alise: What's Windows-only? WIND is only implemented using X
15:50:55 <cpressey> I would prefer something written in pure Befunge that uses ANSI control codes to make a ncurses-y user interface
15:50:55 <Deewiant> 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
15:51:28 <Deewiant> RC/Funge-98 is very non-Windows-only
15:51:40 <ais523> it would be funnier if the software only worked using X on Windows
15:52:04 <ais523> cpressey: yep, and that sort of thing's entirely possible; I just don't think anyone's tried yet
15:52:21 <AnMaster> <cpressey> I would prefer something written in pure Befunge that uses ANSI control codes to make a ncurses-y user interface <-- anything wrong with NCRS?
15:52:33 <AnMaster> for a start "something written in befunge" tends to be very non-reusable
15:52:45 -!- alise_ has joined.
15:52:59 <AnMaster> due to the complete lack of something that works for emulating functions. And even with SUBR it is somewhat messy
15:55:26 -!- alise has quit (Ping timeout: 252 seconds).
15:56:34 <ais523> hmm, is there any Befunge extension that works Modular SNUSP-style?
15:58:11 <ais523> basically, it has commands for subroutine call and return
15:58:21 <ais523> that work like setjmp/longjmp on an explicit stack
15:59:50 <Deewiant> I don't think there's anything quite like that, no
16:00:46 <ais523> it makes subroutining very easy
16:00:53 <ais523> or ofc you could just use IFFI and do subroutines that way
16:01:57 -!- MissPiggy has joined.
16:02:20 -!- MissPiggy has changed nick to fax.
16:02:36 <AnMaster> ais523, you need to port IFFI to work without depending on ick
16:02:48 <cpressey> 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.)
16:02:49 <ais523> that would be "rewrite", not "port"
16:02:52 <AnMaster> of course, since you replace mainloop that would be painful
16:02:53 <ais523> but it's a useful project
16:03:06 <AnMaster> ais523, also, it must work with t
16:03:10 <ais523> the replacing the mainloop is actually not an issue, it's a trivial wrapper
16:03:29 <ais523> 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
16:03:43 <AnMaster> cpressey, I think I joked about a two letter fingerprint NX. That works like the page permissions on hardware
16:03:52 -!- alise_ has quit (Ping timeout: 252 seconds).
16:04:03 <AnMaster> I'm not sure what a write only area would be useful for
16:04:27 <AnMaster> ais523, would be easy to overwrite what you logged though
16:04:27 <ais523> you could read it in a debugger, but not make a security leak
16:04:39 <AnMaster> ais523, I'm not sure that makes sense
16:04:45 <AnMaster> since other threads could still read the data
16:04:46 <cpressey> 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.
16:05:03 <Deewiant> cpressey: MODE has switchmode which is essentially that.
16:05:20 <ais523> cpressey: sounds worryingly like TRDS
16:05:37 <ais523> which could also be very usable for subroutine call/return, if it wasn't for the essential complexity of the whole thing
16:05:38 <Deewiant> Although of course it doesn't work with multiple threads.
16:06:00 <Deewiant> Since it only remembers the latest branch ever, not the latest branch per IP.
16:08:45 <cpressey> Switchmode is close, but it would need to be more elegant, combining in the functionality of w, perhaps.
16:09:34 <Deewiant> What to do with a w that passed through?
16:09:48 <cpressey> Otoh, pretty dispatcher structures are one of the things that make Befunge fun, so why try to make it easy?
16:09:57 <Deewiant> For the other cases, you can single-usely turn it into []
16:10:35 <cpressey> 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.
16:10:54 <Deewiant> But what does reversing == mean
16:11:01 <Deewiant> Since it distinguishes between < and > ordinarily
16:11:07 <Deewiant> You'd have to pick one arbitrarily?
16:11:28 <cpressey> Reversing the path chosen. == chooses the straight line, reversing the straight line still is the straight line.
16:20:09 <cpressey> 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.
16:21:20 -!- ais523 has quit (Remote host closed the connection).
16:21:46 <Deewiant> I think it's somewhat of an excuse to limit the capabilities of your esolang
16:22:52 <Deewiant> 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.
16:36:52 -!- oerjan has joined.
16:38:02 <oerjan> 07:43:52 --- quit: coppro (Quit: I am leaving. You are about to explode.)
16:38:03 <oerjan> 07:44:25 <ais523> coppro's quit message has been false every time so far
16:38:18 <oerjan> well in the long run, if the Big Rip hypothesis is true...
16:46:17 <cpressey> 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)
16:48:01 <cpressey> 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
16:48:12 <cpressey> (Isn't that always the story, though?)
16:49:33 <cpressey> I would like to stand corrected about there not being an implementation
16:50:04 <cpressey> Sgeo does seem to have an implementation of it in Python?
16:50:32 <Sgeo> The file I/O stuff needs some work
16:50:46 <Sgeo> And the spec for the File I/O stuff is probably iffy
16:55:48 <Sgeo> Also, it's untested on Windows
16:56:07 <Sgeo> Although was a major spec change just due to projected issues with Windows
16:59:07 -!- kar8nga has joined.
17:00:40 <cpressey> Having it be a pipeline (and only a pipeline) is definitely the right design, I think.
17:01:18 <cpressey> I haven't unravelled the spec sufficiently to know what I think about the details yet...
17:32:31 -!- tombom has joined.
17:35:58 -!- hiato has joined.
17:38:52 -!- hiato has changed nick to sudobus.
17:39:44 -!- sudobus has changed nick to aqualoqua.
17:39:55 -!- aqualoqua has changed nick to sudobus.
17:40:34 -!- sudobus has left (?).
17:45:17 -!- hiato has joined.
17:45:23 -!- hiato has changed nick to sudobus.
18:01:34 -!- alise has joined.
18:02:17 <alise> Chromium is the devel name
18:02:22 <alise> and all the nasty stuff has options to disab;e
18:03:43 <alise> Gregor: You can set chromium to use OS colours
18:04:03 -!- lament has quit (Ping timeout: 240 seconds).
18:04:28 -!- lament has joined.
18:06:14 -!- alise_ has joined.
18:06:19 <alise_> 21:35:32 <Sgeo> You can always download SRWare Iron
18:06:23 <alise_> You could, but you'd be retarded:
18:06:40 <alise_> http://neugierig.org/software/chromium/notes/2009/12/iron.html
18:08:10 -!- alise has quit (Ping timeout: 252 seconds).
18:08:50 <pikhq> ... He was expecting *money* from that?
18:08:50 <pikhq> Dear God. The money in FLOSS is... Support.
18:09:09 <alise_> fax: you're a fax machine again?
18:09:23 <alise_> pikhq: he got it - see all the publicity
18:09:31 <alise_> I especially like how he removed an entirely innocuous class
18:10:41 <pikhq> If he wanted a real privacy-based browser, he'd do... Something smarter.
18:10:52 <pikhq> Default to incognito, integrate Tor, etc.
18:10:54 <alise_> Best thing to do is just to turn off all the settings in main Chrome.
18:11:14 <pikhq> They're settings for a reason, after all.
18:11:17 <alise_> Google Updater automatic installation.
18:11:22 <alise_> automatic updates = privacy violation
18:11:30 <alise_> Bug tracking system, sends information about crashes or errors.
18:11:36 <alise_> bug reporting = privacy violation
18:11:56 <alise_> A timestamp of when the browser was installed.
18:12:00 <alise_> Oh now /that/ is just insidious
18:12:30 <cpressey> I'm just surprised how candid he was about his real goal
18:12:37 <pikhq> DNS pre-fetching was even *called* insidious?
18:12:46 <alise_> pikhq: oh the lines that aren't factual are my mocking
18:12:52 <alise_> the guy clearly has no idea what he's doing
18:13:13 <cpressey> I submit that he knows exactly what he is doing
18:13:17 <alise_> i read the full log he doesn't understand why people aren't nice to him :-)
18:13:19 <alise_> cpressey: i mean code-wise
18:13:31 <cpressey> Ah. Well there, he barely needs to
18:13:40 <alise_> Also: what means rotful?
18:13:53 <cpressey> Only needs an understanding of what will scare sufficiently paranoid people
18:13:59 <alise_> We haven't had a super-shitty #esoteric meme in ages, and we need one.
18:14:42 <alise_> fax: wow, my brain has completely different heuristic clauses for MissPiggy and fax
18:14:59 <alise_> fax: so I actually read that "hi" completely differently than if you said it before changing your nick back
18:15:13 <alise_> apparently my brain infers huge gobs of meaning into "hi" purely based on who says it
18:15:46 <alise_> permanent nick change or not?
18:16:31 <pikhq> alise_: ... Mine too, oddly enough.
18:17:07 <alise_> hmm... i guess it will take some time for the heuristics to migrate
18:17:19 <alise_> unless you're going to start acting like fax acted too, in which case you'll be two entirely different people
18:18:38 <alise_> 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.
18:19:51 <alise_> cpressey: Obviously the solution is to have it communicate with /its own/ esolang that just does IO stuff.
18:20:02 <cpressey> PSOX seems mostly alright. There are definitely some things that need clarification, and some that I would want to change.
18:20:10 <alise_> *disable (typo from way back)
18:20:29 <alise_> cpressey: Well, it only works with languages that do unrestricted byte-by-byte two-way synchronised binary IO.
18:21:26 <cpressey> alise_: But that's common. If your language communicates with smoke signals, anything like PSOX isn't going to be much help anyway.
18:21:43 <alise_> cpressey: Well, printable ASCII would be a good subset to use...
18:21:48 <cpressey> It looks line-oriented, actually.
18:21:56 <alise_> It's still heavily binary.
18:22:01 <alise_> Also, it's abandoned. I forget why.
18:22:18 <cpressey> Printable ASCII I could live with, but I don't know of any langs that are really crippled from binary I/O?
18:22:36 <alise_> 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.
18:22:46 <alise_> So you place forts and cannons in the right place to aim, and coordinate their firings.
18:22:55 <alise_> cpressey: INTERCAL-72 can only do roman numerals
18:22:59 <Gregor> alise_: OS /colors/ are not the issue. OS /style/ is the issue.
18:23:18 <alise_> so perhaps INTERCAL-72 roman numeral format without over/underlines (so only small numbers) is the lowest common denominator
18:23:26 <alise_> Gregor: Well, you can get the title bar. And it uses GTK widgets inside the page.
18:23:53 <alise_> Gregor: If that isn't acceptable, don't use Chrome :P
18:23:56 <cpressey> alise_: It could look for the first two symbols output, consider them '0' and '1' in binary, and build the rest on that.
18:23:58 <Gregor> If it uses GTK widgets, then why even with "use GTK+ theme" (whatever that means) enabled does it look like friggin' Windows >_<
18:24:10 <alise_> Use GTK+ theme = use its colours
18:24:17 <alise_> And because you don't have a GTK+ theme set up, presumably.
18:24:20 <alise_> So it's using Raleigh.
18:24:24 <alise_> Which looks uber-ugly.
18:24:34 <Gregor> So I most certainly have a GTK+ theme set up.
18:24:39 <alise_> Then it's because you touch yourself at night.
18:24:54 <alise_> More seriously, it's because it's using your title bar colour for a big bit, I imagine.
18:24:54 <Gregor> I touch myself in broad daylight, thank you very much.
18:24:59 <alise_> You could try and edit the settings manually.
18:25:05 <cpressey> 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.
18:25:46 <oerjan> cpressey: you might want it to use the first two _lines_ output
18:25:50 <alise_> cpressey: I think that for most esolangs, fancy programs are /boring/.
18:26:02 <alise_> An IRC client in SNUSP. Whoopdedo,
18:26:07 <alise_> *Whoopdedoo, that's mostly glue.
18:26:18 <alise_> For those where it can be interesting, it's because of an aspect of the language.
18:26:22 <alise_> So you want it part of the language.
18:29:44 <Deewiant> That's along the lines of what I was thinking when I said PSOX makes stuff less interesting
18:31:58 <cpressey> I'm certainly not looking to write a webserver in Hargfak.
18:32:35 <cpressey> I was more thinking of it as a tool to allow esolangs to be more easily passed off as "real".
18:33:21 <cpressey> But if it makes things less interesting, n/m
18:34:46 <cpressey> But on that note, I don't see why most Befunge fingerprints are interesting.
18:37:16 <alise_> In fact, Befunge is relatively uninteresting past its abstract core.
18:37:24 <alise_> Concurrency adds a large gob of fun.
18:37:36 <alise_> Time travel and multiverses add more large gobs.
18:38:22 <cpressey> s/interesting/a popular topic of conversation/, then.
18:38:53 <alise_> "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."
18:38:59 <alise_> http://www.e-pig.org/epilogue/?p=324
18:39:12 <alise_> cpressey: Because the hoi polloi suck at identifying the novel.
18:39:29 <alise_> In fact all the fun in -98 is pretty much the huge sack of implementation woes.
18:39:30 <fax> that post is quite confusing, I don't understand why this doesn't mean epigram is broken
18:39:44 <alise_> they're having to replace W-types with something else
18:39:58 <alise_> otherwise they're fucked
18:40:27 <fax> what confuses me is, whatever they replace W types with: Can't you just implement W with /that/?
18:40:45 <alise_> obviously they have to replace it with something less powerful/abstract
18:40:54 <alise_> http://muaddibspace.blogspot.com/2010/03/algebra-system.html you didn't tell me you had a blog :|
18:41:42 <cpressey> alise_: In that case, Befunge-111 should probably not exist. A clear, unambiguous spec would only ruin the fun.
18:41:49 <fax> because it's embarassing :P
18:42:09 <alise_> cpressey: Well... yeah. Isn't that obvious?
18:42:19 <alise_> You need to introduce a bag of craziness to make it fun, which is why I've been pushing my idiocy.
18:42:44 <alise_> fax: hmm... I agree that ZFC is probably inconsistent, yet I'm having some sort of knee-jerk AARGH NO reaction to its statement
18:43:49 <alise_> fax: I think I've read a post on your blog before and it was ridiculously overcomplicated for something
18:44:19 <uorygl> What's this about ZFC being inconsistent?
18:44:35 -!- MizardX has quit (Read error: Connection reset by peer).
18:44:40 <alise_> uorygl: it probably is
18:45:23 <alise_> http://r6.ca/blog/20091101T231201Z.html
18:45:31 -!- MizardX has joined.
18:45:42 <alise_> but if you belong to general dependent-type constructivist cabal, then yeah probably :P
18:45:54 <alise_> fax: of course you forgot to add "for the same reasons that Coq is probably inconsistent".
18:45:59 <fax> alise: Today I just picked up "Constructive Functional Analysis"
18:46:33 <cpressey> "Can we really believe in the consistency of any system whose ordinal strength we do not have a notation for?"
18:46:49 * fax can't interpret that '...'
18:47:06 <alise_> Probably "That's ridiculous, either p or not p"
18:47:15 <alise_> (Note: Above sentence is merely mocking the mocking of the classicalists.)
18:48:14 <alise_> fax: Ah yes, I think it was your thing on halving numbers
18:48:27 <fax> I thought it might be that
18:48:35 <alise_> cpressey: Inner meaning?
18:48:57 <cpressey> Maybe I'll eventually figure out the words for the thought, but don't expect it soon.
18:50:07 <alise_> cpressey: Fundamental thought, generalised, is "I agree", "I disagree" or "<shock, dunno>"?
18:50:42 <cpressey> Honestly, my inclination was to respond with "Please, won't somebody think of the children??!?!"
18:50:48 <uorygl> 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.
18:50:58 <alise_> fax: you object to insulting wolfram? :|
18:51:05 <cpressey> But I am sensitive to overusing Simpsons quotes.
18:51:13 <fax> stop stalking me!!
18:51:17 <alise_> uorygl: Oh yes it does!
18:52:28 <alise_> hey gloss is exactly what i need for my othello program i think
18:52:33 <alise_> can it do mouseclicks, I wonder
18:53:15 <fax> I'm reading about finite calculus right now, though
18:53:41 <fax> the discrete derivative of f at x is defined as f(x+1)-f(x)
18:53:54 <cpressey> What would it mean for ZFC to be inconsistent? In practical terms, I mean.
18:54:34 <uorygl> It would mean that in ZFC, it's possible to prove anything at all, making all theorems proved in ZFC meaningless.
18:55:31 <alise_> 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.
18:55:31 <cpressey> 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.
18:55:42 <fax> alise you know I have a soft spot for people like wolfram
18:55:54 <alise_> fax: I don't actually.
18:56:19 <cpressey> I do. It's a beanbag chair in a dungeon.
18:56:27 <alise_> fax: Personally, the way he reacted to ais523's solving of the Wolfram prize gives it a slightly personal edge to me.
18:57:01 <alise_> "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 ..."
18:58:40 <fax> did he mistreat ais in some way?
19:00:28 <alise_> 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.
19:01:34 <cpressey> Even before I knew that, he rankled me immensely.
19:03:40 <alise_> 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.
19:04:17 <cpressey> 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".
19:04:28 <alise_> fax: I'll find it; sec.
19:05:00 <alise_> fax: For now, he's Feynman writing to Wolfram (warning: surrounded with wolframlove by the transcriber) http://elzr.com/posts/wolfram-feynman
19:07:06 <cpressey> If ZFC was inconsistent, there would be chains of reasoning in it which did not terminate, correct?
19:07:16 <alise_> cpressey: You are thinking in computational terms.
19:07:23 <alise_> Inconsistency means that you can prove a falsehood.
19:07:32 <alise_> This is a contradiction.
19:07:33 <cpressey> alise_: As is my perogative, I thought.
19:07:47 <alise_> From this, you can prove anything.
19:08:15 <alise_> 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.
19:08:16 <cpressey> If you can prove anything, you can prove the premises, therefore there are chains of reasoning which do not terminate.
19:08:22 <Deewiant> See http://xkcd.com/704/ for an example
19:08:43 <alise_> Deewiant: I liked that xkcd - incredibly rare for me as of late.
19:09:09 <alise_> 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
19:10:08 <alise_> cpressey: In the dependent-types view, we hvae
19:10:29 <alise_> If you prove a falsehood, your value doesn't terminate when evaluated.
19:10:38 <Gregor> alise_: The most recent xkcd was REALLY bad.
19:10:41 <alise_> So, yes, in a way you are right.
19:10:42 <cpressey> I'm not convinced of the converse, though (If there are chains of reasoning which don't terminate in ZFC, then it's inconsistent)
19:10:46 <Gregor> So bad I may remove it from my RSS reader.
19:10:47 <alise_> But "termination" doesn't make any sense in logic.
19:10:56 <pikhq> Deewiant: Yeah, that was an enjoyable xkcd.
19:10:59 <alise_> Infinite chains of reasoning, perhaps, but there is no computation, so there is no termination.
19:11:34 <cpressey> alise_: You have a computational view of "termination", I think.
19:11:34 <pikhq> I read xkcd still because *following* a hit-and-miss comic takes very little time.
19:11:45 <alise_> cpressey: Right you are.
19:11:50 <pikhq> Once I've started following a comic, it takes a severe facepalm moment for me to stop.
19:11:55 <pikhq> ... Or just severe apathy.
19:11:57 <fax> oklokok, hi
19:12:21 <Gregor> pikhq: Yeah, but this latest one was terrible, even for XKCD.
19:12:26 <Gregor> Like, ow, my brain hurts terrible.
19:13:53 <uorygl> cpressey: what do you mean by "chain of reasoning"?
19:14:04 <pikhq> Gregor: True. It did quite suck.
19:14:13 <uorygl> This looks like a non-terminating chain of reasoning to me: 1 = 1; therefore, 2 = 2; therefore, 3 = 3; therefore, 4 = 4; therefore, . . .
19:14:29 -!- alise has joined.
19:14:44 <Deewiant> Or just "1 = 1 therefore 1 = 1 therefore ..."
19:14:57 <alise> 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"
19:15:23 <pikhq> alise: ... I think I scrubbed it from my memory.
19:15:38 <cpressey> uorygl: AFAICT that's what I mean.
19:15:57 <fax> hey I've hated xkcd for years
19:15:59 <uorygl> cpressey: okay, so I just showed you a non-terminating chain of reasoning. So does that mean ZFC is consistent?
19:16:00 -!- alise_ has quit (Ping timeout: 252 seconds).
19:16:02 <fax> how come you guys are only just catching up now
19:16:02 <alise> cpressey: imo proofs aren't actually part of zfc's truth space
19:16:14 <alise> fax: it started sucking around maybe 2007-2008 imo.
19:16:21 <cpressey> You have axioms and rules for deriving theorems from those axioms.
19:16:25 <alise> cpressey: as in they're just a tool for us to reason about, and verify things
19:16:35 <alise> but they're totally orthogonal to any issue actually related to the set of truths we call zfc
19:16:36 <pikhq> fax: Because it's gone from overrated but amusing to overrated and sucking most of the time.
19:17:19 * sudobus liked it better when the convo was about stuff he knew about, like the cocio-economic effects of a potential utube cencorship, or cats
19:17:41 <cpressey> uorygl: No, that's the converse that I said I wasn't convinced of, isn't it?
19:17:54 <fax> "utube" ;_;
19:18:13 <alise> sudobus: you do realise this is a progrmaming channel :)
19:18:22 <cpressey> <cpressey> I'm not convinced of the converse, though (If there are chains of reasoning which don't terminate in ZFC, then it's inconsistent)
19:18:33 <uorygl> cpressey: so now are you convinced that the existence of a non-terminating chain of reasoning doesn't imply that it's inconsistent?
19:18:54 <cpressey> uorygl: Other way 'round. If it's inconsistent, then etc
19:18:59 <pikhq> sudobus: Spelling. Improve it.
19:19:13 <alise> pikhq: he's south african he can do what the hell he likes because he's interesting
19:19:17 <alise> sudobus: I know what a catbus is, but what's a sudobus?
19:19:20 <fax> IRC has just enough people who spell things correctly to make it really depressing when someone comes out with shit like "cong@l8"
19:19:46 <alise> fax: here's wolfram being a complete idiot http://groups.google.com/group/comp.lang.lisp/msg/f3b93140c2f2e922?dmode=source&output=gplain&pli=1
19:20:06 <uorygl> I think you mean "çocio-economic" and "cençorship".
19:20:20 <sudobus> 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
19:20:24 <Deewiant> Most people are complete idiots at least a couple of times in their lives
19:20:34 <pikhq> I think he meant γ€γ¨γ¦γ€γγγ‘γ.
19:20:39 <pikhq> (note -- not actual Japanese)
19:20:40 <fax> alise, ah this is KMP -- I have read this
19:20:45 <cpressey> Deewiant: Yes, it takes a very special sort of person to make a career out of it.
19:22:07 <alise> Deewiant: It shows that Wolfram has a huge attitude problem & ego that has lasted til today.
19:22:10 <fax> He then said "I'm going to read these and then I'll know as much as you."
19:22:26 <sudobus> alise: I just realised I left out at least a word from my previous reply. Note: rest a mirror ... just right so that the ..
19:23:35 <uorygl> I actually am going to read these, and then I actually will know as much as you!
19:24:25 <fax> I should carry about a stack of books just incase I want to insult someone
19:25:40 <cpressey> including "the compiler book with the dragon on it"
19:26:09 <pikhq> Tangentially, I should read the Dragon Book sometime.
19:26:16 <fax> why? it's outdated
19:26:23 <fax> you would only read if you like history
19:26:38 <fax> Appels book
19:26:39 <pikhq> ... Outdated books can be enjoyable.
19:27:02 <pikhq> Or at least enlightening.
19:27:26 <Deewiant> fax: The latest edition of the dragon book is newer than Appel's
19:27:40 <pikhq> Oh, and there have been 2 later editions.
19:27:43 <pikhq> Most recent was in 2006.
19:27:56 <pikhq> Of course, most people think of the *first*, but still.
19:28:08 <fax> ah that's interesting
19:28:20 <fax> they have republished it, I have not seen the new version
19:28:28 <cpressey> I've heard the recent editions are not much more than reprints of the originals?
19:28:31 <pikhq> Deewiant: Yeah, yeah.
19:28:36 <alise> there aren't any compiler books from a functional perspective
19:28:53 <Deewiant> alise: "Modern Compiler Design" explains a bit of how Haskell is compiled
19:28:58 <cpressey> alise: "Modern Compier Design"... yeah
19:29:08 <alise> structuring compilers functionally
19:29:12 <fax> alise, Calculating Compilers
19:29:12 <cpressey> MCD's coverage is not very good though
19:29:24 <fax> (PhD thesis, but it's a good read anyway)
19:29:27 <alise> fax: well... foo to you
19:29:31 <pikhq> alise: The Implementation of Functional Programming Languages, by SPJ?
19:29:56 <cpressey> Part of me wonders why you even need a book on it :/
19:29:57 <fax> alise, http://www.reddit.com/r/squiggol/
19:30:06 <alise> cpressey: Sexy purposes
19:31:20 <alise> http://www.uni-koblenz.de/~laemmel/expression/long.pdf cool, material on the expression problem!
19:31:23 <cpressey> Proving compilers correct is useless.
19:31:33 <fax> cpressey, hahahahah
19:31:33 <cpressey> Prove the generated code is correct.
19:31:40 <alise> cpressey: That's... what you do.
19:32:08 <pikhq> cpressey: ... That's not the only reason to write a compiler functionally...
19:32:14 <pikhq> Or write anything functionally...
19:32:15 <cpressey> A correct compiler will take an incorrect program and produce another incorrect program.
19:32:17 <alise> You prove that the canonical semantics of the input (syntax tree) are equivalent to the canonical semantics of the output.
19:32:19 <fax> "Proving compilers correct is useless." -- I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a remark.
19:32:25 <pikhq> And... That's... What people do...
19:32:25 -!- sudobus has quit (Quit: leaving).
19:32:43 <cpressey> fax: Some of it is overstatement. But not all of it.
19:32:45 <pikhq> cpressey: Why yes. Yes it will.
19:32:54 <fax> 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.
19:33:05 <pikhq> cpressey: And I would expect nothing more of a correct compiler.
19:33:20 <pikhq> Well. I also want correct code to produce correct output.
19:33:43 <alise> So, dependently-typed combinator calculus.
19:33:57 <alise> Specifically: a language with only combinators that has dependent types and is total (but not powerless).
19:34:01 <alise> (No lambda abstractions.)
19:34:03 <fax> alise answer me!
19:34:04 <cpressey> 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.
19:34:22 <fax> alise from earlier
19:35:12 <pikhq> cpressey: It's fairly simple -- when your compiler is *incorrect*, you cannot rely on the compiler to generate correct code.
19:35:21 <fax> ugh alise why are you so mean
19:35:30 <alise> fax: I'm not, I just don't know what the fuck you want me to do
19:35:50 <alise> 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
19:36:39 <alise> 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".
19:36:46 <cpressey> pikhq: Right, so proving programs correct is important. I get that.
19:36:51 <alise> So proving the compiler correct /is/ proving the compiler's output correct.
19:37:03 <cpressey> What I don't get is why this *special case* is so friggin' popular, esp. in theses.
19:37:29 <alise> because it's hard.
19:37:32 <fax> alise, you just seem to sort of phase out when I link you stuff
19:37:35 <alise> see e.g. Reflections on Trusting Trust
19:37:43 <pikhq> cpressey: Because it's more important than most other cases.
19:37:45 <alise> fax: no I just don't respond to links that I am unable to interpret the context of; also, I did respond
19:37:49 <alise> I linked to an article linked to in that subreddit
19:37:53 <pikhq> Since almost everything is compiled.
19:38:01 <fax> alise, no there's a compilers book in there
19:38:24 <cpressey> Yet ultimately, everything is interpreted.
19:38:43 <cpressey> We should probably be proving our text editors correct, too.
19:40:32 <alise> Do you have any idea how much verification goes into making an x86 CPU?
19:40:33 <fax> cpressey, http://jaguar.it.miami.edu/~chris/formal_methods_in_the_movies/TheWizardOfOz.html
19:41:17 -!- alise_ has joined.
19:41:24 <pikhq> alise: Issues still slip on through on occasion, though.
19:41:35 <pikhq> Though the only such case I can think of is the FDIV bug on the Pentiums...
19:41:48 <alise_> 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.
19:42:01 <alise_> pikhq: Which is basically the reason WHY they do formal verification nowadays.
19:42:26 <alise_> cpressey: For compilers, Reflections on Trusting Trust shows that it is pretty much /unknowable/ whether a compiler is correct.
19:42:45 <alise_> Even if the compiler is not malicious, such errors could happen. And verifying that a huge program was compiled correctly? Good luck.
19:42:53 <alise_> So we attack the problem at the source, and prove our compiler correct.
19:43:19 <AnMaster> how does one get a degree sign in LaTeX?
19:43:40 <cpressey> 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.
19:44:23 <alise_> cpressey: You don't understand - given a black-box compiler proving that your code was compiled correctly is almost impossible.
19:44:33 <Deewiant> AnMaster: See also http://detexify.kirelabs.org/classify.html
19:44:48 <alise_> 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.
19:44:53 <alise_> Voila, the compiler is Always Right.
19:44:58 -!- alise has quit (Ping timeout: 252 seconds).
19:45:01 <fizzie> I think I saw ^\circ used somewhere, yes.
19:45:02 <alise_> cpressey: If we just have the input, and the output... where do you start?
19:45:03 <Deewiant> AnMaster: I.e. raise it to the power of one circle :-P
19:45:09 <alise_> You have to model how it was compiled first - basically, write your own compiler.
19:45:15 <fax> "we do it by meticulously analysing every case it uses to compile constructs" -- *sigh*
19:45:18 <alise_> Then you have to verify that each compilation is equal to how your model would compile it.
19:45:30 <alise_> cpressey: But then we have to verify our now-very-real model compiler is correct, or it's useless.
19:45:34 <cpressey> alise_: You have the semantics of the program, and you have the semantics of the target language. That's where you start.
19:45:50 <fax> have you every actually done a formal correctness proof for a non-trivial compiler?
19:46:12 <fizzie> http://anthony.liekens.net/index.php/LaTeX/DegreesNotation -- that suggests either ^\circ (possibly with your own \newcommand) or the existing \degree from \usepackage{gensymb}.
19:46:20 <alise_> fax: Would you prefer I went into the nitty-gritty when the abstarct principles are all that matter here?
19:46:26 <cpressey> fax: Me? No. But (as should be obvious) I have reasons for that.
19:46:36 <fax> cpressey, not you, alise :p
19:46:36 <alise_> fizzie: I was thinking ^\circ. Thought it'd be too silly to say.
19:46:52 <fizzie> It's less silly than just ^o at the very least. :p
19:47:16 <cpressey> fax: For trivial compilers, the problem seems not too difficult, maybe even enjoyable if the compiler is written a certain way
19:48:27 * fax needs alise to get into the trenches
19:49:40 <alise_> fax: But my ivory tower is so comfortable...
19:49:56 <alise_> Besides, I refuse to do any serious work in anyone ELSE's language. They have cooties.
19:54:51 <cpressey> 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.
19:55:29 <cpressey> If a->b is correct, and c->d is correct, (a,c)->(b,d) is correct, assuming sane composition
19:56:26 <alise_> cpressey: Now add full-program optimisations.
19:56:44 <cpressey> Oh yes. The problem AS USUAL is that someone wants it to GO FAST.
20:00:57 <fax> this is not accurate
20:01:50 -!- alise_ has quit (Ping timeout: 252 seconds).
20:02:25 -!- alise has joined.
20:02:35 <alise> cpressey: Mind you, I don't plan on including a clever compiler in my OS.
20:02:46 <alise> It's near-the-metal, and cpus are really fast. So...
20:04:09 -!- lament has quit (Ping timeout: 260 seconds).
20:06:38 <cpressey> I'm simply disregarding all considerations of efficiency.
20:07:00 <cpressey> Waste of time to worry about wasting time.
20:07:20 -!- lament has joined.
20:07:59 <olsner> cpressey: ah, words of truth
20:09:15 <cpressey> 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.
20:11:00 <cpressey> http://dadgum.com/james/performance.html
20:15:39 <cpressey> alise: Why are you writing an Othello in Haskell?
20:21:24 <alise> I need type-level functions.
20:21:41 <alise> ...because I'm implementing a dependently-typed language. :-)
20:21:50 <alise> (But not for /that/ reason.)
20:23:09 <oerjan> othello and its rich internal type system...
20:24:03 * alise steps back, examines his general structure.
20:24:14 <alise> Lam :: (Id a -> LC b) -> LC (a :-> b) was so nice, too. Sigh.
20:24:29 <oerjan> so you Lam-ent its loss?
20:24:32 <alise> You could even Show it.
20:25:03 <cpressey> I don't believe in ZFC, I don't see why I should believe in dependent types.
20:25:47 <alise> \(x:T).(e:R) : pi (x:T). R
20:26:08 <fax> alise why don't you write it in Coq (type functions!) then extract it to haskell
20:26:12 <alise> (f : pi (x:T). r) v : r[x=v]
20:26:16 <fax> if you do that it'll be a really sweet hack
20:29:17 <fax> use monads !
20:30:23 <oerjan> everything's better with monads!
20:30:58 <alise> sem' xs (App f x) = (sem xs f) (sem xs x)
20:31:07 <alise> App :: LC (a β> b) -> LC a -> LC b
20:31:23 <alise> I guess I need to specifically specify f must be a Lam
20:31:47 <alise> fax: de bruijn housekeeping
20:32:02 <alise> actually I think it needs to be a function... maybe
20:32:42 <alise> against inferred type `[(.) (forall a1) (LC a1)]'
20:37:40 <alise> fax: sem' :: (Id t -> t) -> LC a -> a
20:37:44 <alise> sem' v (Var i@(Id n :: Id t)) = v i :: t
20:37:46 <alise> why doesn't this work :(
20:39:02 <fax> something to do with needing to enable a bunch of extensions that should really be the default?
20:39:45 <alise> Couldn't match expected type `t' against inferred type `a'
20:40:16 <fax> do sem' :: (Id a -> a) -> LC a -> a :D
20:40:22 <alise> (forall t. Id t -> t)
20:40:30 <fax> how can that be the right type?
20:40:34 <fax> what's Id t?
20:41:07 <fax> can you implement (in a pure and safe way) STRefs this way?
20:43:43 -!- alise_ has joined.
20:44:44 -!- alise has quit (Ping timeout: 252 seconds).
20:53:01 -!- oerjan has quit (Quit: Good night).
20:54:07 <alise_> othello is more fun than this
20:54:35 <alise_> fax: I assume there's some hyper-monoidal structure for game boards :-P
20:58:12 <alise_> fax: Reifying without _|_:
20:58:13 <alise_> instance (TNat n) => TNat (S n) where reify _ = 1 + ((reify :: (n -> n) -> Integer) id)
20:58:38 <alise_> In fact, you could even have reify :: Dummy n -> Integer where (data Dummy t = Dumb)
20:59:09 <alise_> Dummy is basically values indexing on types :P
21:17:34 <alise_> 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 :)
21:19:26 <fax> well I am interpreting 'elide' in a special way
21:23:15 <fax> yeah and prove them
21:24:27 <alise_> fax: http://www.reddit.com/r/dependent_types/comments/baf7g/wtypes_good_news_and_bad_news_laquo_epilogue/ why epigram 2 isn't broken
21:25:04 <fax> from the murky depths http://sneezy.cs.nott.ac.uk/darcs/RDTP/2ndmeeting/ctm-3.JPG ...
21:27:21 <alise_> fax: btw I think I understood your thing about induction from the logs
21:27:29 <alise_> so what is mu-elim's actual type, I'm curious?
21:27:38 <alise_> admittedly this is the rough kind of understanding, not the deep kind
21:28:35 <AnMaster> every X process ended up as STOPPed
21:28:48 <AnMaster> killall -CONT <huge list> seems to have helped *somewhat*
21:30:07 <AnMaster> except I can't resume that dbus crap
21:30:16 <AnMaster> it causes everything else to SIGSTOP again
21:32:19 <alise_> I should really devise a way to isomorph the pure data types with an efficient implementaiton.
21:33:39 <cpressey> I once read a PhD thesis were 70% of the ~200 pages was a transcript of a session with an interactive proof system.
21:35:22 <AnMaster> it all started when inkscape crashed
21:35:31 <AnMaster> it seems that resulted in dbus crashing or something
21:35:52 <AnMaster> ooh nice, gconfd is eating 100% CPU
21:38:39 -!- MigoMipo has quit.
21:39:39 <alise_> cpressey: Formalised proofs are the future!
21:39:44 <alise_> Although a transcript is probably not the best form.
21:40:02 <fax> formal math is so difficult
21:40:24 <fax> but it's different than proving stuff on paper, and it's a bit different than programming too
21:40:34 <fax> it's a bit perverse
21:48:36 <cpressey> 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.
21:48:54 <AnMaster> how do you prevent LaTeX from including a date on the title page?
21:49:56 <alise_> proof checker = type checker
21:50:33 <fax> proof checker is simple? :)
21:50:37 <fax> yes that is true
21:50:43 <fax> but it is hard to write proofs :P
21:51:10 <fizzie> AnMaster: Use \date{} -- though it might be suboptimally spaced.
21:51:38 <AnMaster> fizzie, hm spacing is important since I don't use a separate title page
21:52:37 <fizzie> 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.
21:52:50 <fizzie> It's possible that it's clever enough to detect and special-case an empty date.
21:53:36 <alise_> someone (fax) gimme the interpretation brackets
21:53:59 <alise_> qwrtuc6ybpoi;ytrweaqstr4jy;poin0[;qwo'm[pn;iqw;p0oi[ie3ye3wdrty;piyuhtw2qwqaretshygu,-';juytdrtuh0poesr48#'[p0oiyhtdryk]='
21:54:16 <fax> you dirty qwerty user!
21:56:53 -!- Oranjer has joined.
21:57:45 <alise_> coq proofs don't look nearly enough like real mathematical proofs
21:58:04 <alise_> kazonk; whup f; bop; ligxs
21:58:13 <alise_> Theorem prover, programming language.
21:59:43 <fax> alise they shouldn't look like what you find in textbooks
21:59:59 <cpressey> Trivial example of what I have in mind: http://dpaste.com/169655/
22:00:20 <fax> alise, well it has been pointed out by Freek that these proof assistants do look very much like Euclids Elements in style
22:00:30 <fax> but I mean on paper stuff is a different world
22:00:44 <alise_> yeah but it shouldn't be a different world!
22:00:55 <fax> paper can't compute (yet!) :P
22:01:13 <alise_> imo we should all be using dependent formal proofs everywhere
22:01:28 <alise_> and with say coq proofs that is .. not practical
22:02:10 <fax> more of your bullshit
22:03:15 <alise_> fax: you can just not listen to me, you know
22:04:10 <Oranjer> but ignoring people is the center that all totaltarianism revolves around!
22:04:20 <cpressey> Dude, we're still grappling with sophisticated SE concepts like "comments" and "tests"
22:07:28 <cpressey> I am currently trying to add a feature to a swath of our code that another engineer accurately described as an "accretion"
22:07:57 <cpressey> 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"
22:08:50 <cpressey> 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"
22:09:43 <alise_> Programming is a shithole/
22:10:24 * AnMaster uses a -1.5 em vertical spacer and then violently hits LaTeX with it
22:11:34 <AnMaster> 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
22:11:35 <cpressey> We don't even have debuggers that aren't crap. (Where did this value come from? Tell me. No, you can't, can you.)
22:11:50 <AnMaster> fizzie, wonderfully hackish in factr
22:14:03 <fizzie> I tend to often end up with some negative spaces here and there too, though I always feel I'm doing something wrong.
22:14:05 <alise_> Actually you've made me think: perhaps debuggers are isomorphic to proof assistants.
22:14:14 <alise_> (Except you never get around to proving anything.)
22:14:32 <cpressey> alise_: They're certainly related.
22:16:01 <cpressey> You need to visualize the innards to see why the end result is not what you expected.
22:16:30 * fax visualize your innards
22:16:50 <AnMaster> fizzie, actually that wasn't just a negative space. it was a -6 em vertical spacer at the top of a mini page
22:17:00 <AnMaster> to "fake" it being at level with the other one
22:17:31 <AnMaster> somehow the display style equation in that mini page caused it to fill out the whole page when it came to vertical placement
22:19:21 <Gregor> Chrome's search feature is a suckfest ... and not the good kind.
22:20:12 <alise_> Just type in what you want and press enter. ...Hooray.
22:20:29 <alise_> Or if you're going to search for something that looks like a URL, ?poop://lol<ENTER>.
22:20:39 <alise_> I think there's even a shortcut for Ctrl-L + ?
22:20:41 <Gregor> Nonono, search on a page, its "find" feature
22:20:54 <Gregor> Whatever you want to call it.
22:23:18 <Gregor> 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 >_<
22:28:19 <alise_> Gregor: (1) Oh, Ctrl-F, how horrible. (2) Okay.
22:28:28 <alise_> AnMaster: No. Because it's meant for people to use. Quickly.
22:28:35 <cpressey> 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.
22:28:40 <Gregor> Ctrl is a lot farther from the home row than / is, if searching is common then it's annoying.
22:28:48 -!- tombom has quit (Quit: Leaving).
22:28:58 <Gregor> 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 ...
22:29:15 <alise_> Gregor: Chrome is a bit mouse-based. There's an extension that lets you do /foo and the like.
22:29:54 <alise_> http://github.com/philc/vimium
22:31:07 <AnMaster> alise_, you know, I quite often use egrep as a quick way to search
22:31:15 <alise_> AnMaster: you are not technicaly human though.
22:31:25 <AnMaster> alise_, neither are you if you know any regex
22:31:51 <pikhq> Gregor: Ctrl is *on* the home row.
22:32:05 <Gregor> pikhq: Screw you Unixy Solaris keyboard
22:32:28 <pikhq> AnMaster: I just xmodmap'd.
22:32:39 <alise_> 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
22:32:49 <alise_> (I'm trying to formulate all IO as one single interaction axiom.)
22:33:43 <pikhq> alise_: Uniqueness type?
22:33:56 <alise_> pikhq: Thanks for complicating up my theory :P
22:34:25 <alise_> basically, (World s) represents a world with conditions s
22:34:44 <alise_> (Interaction p f t) is an interaction on worlds; p is Conditions -> Prop
22:34:52 <alise_> meaning "is this interaction acceptable under these conditions?"
22:35:05 <alise_> for instance, a read-from-stream interaction would have a p representing that the buffer must be open in the world
22:35:11 <alise_> f is Conditions -> Conditions
22:35:17 <alise_> representing the effect it has on the conditions of the world
22:35:28 <alise_> a close-stream interaction would require that the stream be open in p, and make it closed in f
22:35:35 <alise_> and t is the type of the result it returns
22:35:50 <alise_> dependent types would mean that closing an already-closed file would actually be a type error.
22:36:51 <alise_> conor mcbride did some sort of thing on this i know
22:37:51 <alise_> heh i'm actualy reading idris stuff now
22:37:57 <alise_> maybe the issue is World
22:40:18 <alise_> fax: how does idris do it?
22:41:47 <fax> theres papers on it
22:42:01 -!- kar8nga has quit (Remote host closed the connection).
22:42:02 <alise_> yeah but i can't find them
22:42:32 <fax> http://www.cs.st-andrews.ac.uk/~eb/drafts/tfp08.pdf
22:42:35 <fax> http://www.cs.st-andrews.ac.uk/~eb/drafts/ngna2009-dsl.pdf
22:42:51 <cpressey> Make a dependent type system where trying to unserialize a corrupt string is a type error!
22:45:00 <alise_> cpressey: Possible but a bit useless since you have to prove it.
22:45:13 <alise_> So you'll basically do if corrupt x then fail else yay (long proof)
22:45:26 <alise_> Better to have the serialiser return, say, Maybe DeserialisedType
22:46:44 <AnMaster> <alise_> dependent types would mean that closing an already-closed file would actually be a type error. <-- anything wrong with that?
22:46:46 <alise_> fax: Just to confirm. http://www.cs.st-andrews.ac.uk/~eb/drafts/tfp08.pdf is not about interaction, yes?
22:46:53 <alise_> I skimmed it and didn't see anything related.
22:46:58 <alise_> AnMaster: It's a good thing. Duh.
22:47:48 <cpressey> What about failing to close a file?
22:48:18 <cpressey> 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.
22:49:08 <alise_> cpressey: Actually, yeah, you could.
22:49:25 <alise_> Make interact continuation-y and require that the world yielded by the continuation satisfies another bit of the Interaction.
22:49:26 <AnMaster> cpressey, also closing a file could fail
22:49:36 <alise_> open-file would have as its ever-ever-postcondition that the file is closed.
22:49:56 <AnMaster> cpressey, isn't fclose() in C allowed to fail if data is buffered but there is no space to write it?
22:50:21 <pikhq> Yes, fclose() can fail.
22:50:34 <AnMaster> so, well you could have to propagate some such errors to your high level language
22:52:20 -!- oklokok has quit (Read error: Connection reset by peer).
22:52:38 <AnMaster> <cpressey> Scylla and Charybdis <-- ?
22:52:46 <AnMaster> the latter means "ircd software" to me
22:53:01 <AnMaster> (the one freenode uses nowdays is based on charybdis)
22:54:45 <alise_> No, the other Scylla and Charybdis.
22:55:37 <AnMaster> 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.]?
22:56:27 <alise_> No, the other Scylla and Charybdis.
22:56:58 <AnMaster> alise_, I only get idiom and mythology hits on my first two results pages
22:57:22 <AnMaster> alise_, so what the heck are you talking about
22:57:49 <alise_> The other Scylla and Charybdis.
22:57:58 <AnMaster> alise_, there is no such hit for me
22:58:07 <alise_> The other Scylla and Charybdis.
22:58:50 <AnMaster> okay, now you are just trolling
23:00:00 <alise_> It's not my fault you're an idiot.
23:00:35 <AnMaster> for not figuring out you were trolling sooner? perhaps
23:00:59 <AnMaster> I had a hard time imaging you were trolling at first.
23:01:01 <cpressey> For convenience, this function may accept either a string, a list, a dictionary, or a file.
23:01:53 -!- madbr has joined.
23:02:54 <alise_> cpressey: Ever considered just becoming a hermit?
23:02:57 <alise_> A hermit with internet access.
23:04:31 <cpressey> Well yes, if it wasn't for the whole property-tax thing.
23:05:09 <alise_> cpressey: Caves. They have none.
23:05:37 <cpressey> Then there's that whole evading-park-rangers thing.
23:06:39 <alise_> cpressey: Beats 9-5, right?
23:07:21 <cpressey> Totally. I should have gone to Hermit School when I had the chance...
23:08:15 <alise_> I'm basically banking on becoming a tenured professor because of my sheer genius without trying at some point.
23:09:02 <cpressey> Well, then practise backstabbing now, is my advice.
23:09:12 <cpressey> You'll need it in grad school.
23:10:29 <alise_> Remember when I said sheer genius?
23:10:33 <alise_> I'll do it and NOT EVEN REALISE IT.
23:10:43 <alise_> Set myself to auto-pilot, baby.
23:12:28 -!- oklokok has joined.
23:12:32 <fax> ho oklokok
23:12:44 <fax> alise tenured how?
23:13:12 <alise_> the badass kind that means I can do nothing and never get fired
23:13:17 <alise_> (note: I do not actually believe any of this0
23:13:29 <fax> like Zeilberger
23:14:21 <fax> "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"
23:14:33 <cpressey> "Zeilberger considers himself an ultrafinitist." Wow, they actually exist??
23:14:46 <fax> yeah so I do
23:15:00 <madbr> ultrafinitist? what does that even mean?
23:15:04 <fax> I don't beleive that a^b terminates
23:15:45 <alise_> 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
23:15:56 <alise_> It's like argument by lack of imagination
23:16:12 <alise_> Argument by well our current computers can't do it/well our current understanding of physics means we can't do it
23:16:15 <cpressey> Or by vagary in definition of "exists"
23:16:20 <alise_> fax: surely you don't consider yourself such.
23:16:45 <pikhq> I can in fact produce an object that is of some arbitrary numerical length. By defining the units appropriately.
23:16:47 <alise_> So ultrafinitists believe there to be a largest number. I wonder what it is :)
23:17:13 <pikhq> For instance, I have a meter stick that is roughly G 1/G-meters.
23:17:24 <cpressey> I'm not completely alien to their ideas, but I don't think I am one
23:17:27 <Sgeo> Who pinged me?
23:17:44 <lament> alise_: the largest number is 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875897
23:17:57 <alise_> lament: 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875898
23:17:59 <pikhq> lament: 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875898
23:18:15 <lament> just a meaningless string of digits
23:18:21 <fax> oh lament is a 9872364578691826349876985702349785018923478962345987697812340123408723984568347691698273649852394875897-finitist
23:18:29 <madbr> you could argue that numbers larger than X don't have any practical use, that's kinda dumb
23:18:33 <pikhq> It's the successor of the largest number you proclaimed.
23:18:36 <lament> it doesn't mean anything. Numbers can't be that large.
23:18:47 <pikhq> lament: Define number.
23:18:52 <fax> I'm a 2^16-finitist
23:19:16 <alise_> fax: lament thinks such a finitism doesn't exist
23:19:17 <pikhq> data Number = Zero | Succ Number
23:19:48 <fax> pikhq, fix Succ -- where is your arithmetic now?
23:19:58 <fax> lament, ask #haskell :x
23:20:09 <lament> why? I'm more qualified than #haskell
23:20:12 <pikhq> fax: Congrats, you just defined infinity.
23:20:15 <fax> why doesn't oklocorpse talk to me :(
23:20:17 <lament> i've a math degree, most people in #haskell don't.
23:20:21 <fax> oklokok oklokok oklokok
23:20:33 <alise_> _|_Nat is not infinity
23:20:59 <pikhq> alise_: Fine, fine. He's defined _|_ :: Number.
23:21:10 <fax> lament: hey did you specialize?
23:21:15 <fax> at some point
23:21:18 <AnMaster> <fax> why doesn't oklocorpse talk to me :( <-- I guess he got tried of saying BRAAAINS?
23:22:53 -!- oklokok has quit (Ping timeout: 260 seconds).
23:23:45 -!- oklokok has joined.
23:24:00 <madbr> damn postmodernists
23:26:00 <cpressey> Ο exists because I can describe it (I can describe Atlantis too)
23:30:08 <alise_> Ο is shorthand for some definition in some system of axioms. in those, it is presumably a coherent concept
23:30:22 <alise_> the problem is that you want Atlantis to be a concept of this world. and we don't control /our/ axioms.
23:30:48 <cpressey> God no, I don't want that. They would cream us with their nuclear laser missiles!
23:31:21 * fax sighs there are so many things I want to do that I am unable to do any of them
23:31:42 <alise_> I love how the Halting Problem is equivalent to the Entscheidungsproblem.
23:32:04 <fax> yeah that's a good one
23:34:27 <alise_> decide : (βa. Prog a β Bool) β (P : Prog (Nat β Bool)) β Bool
23:34:28 <alise_> decide H P = Β¬(H γi := 0. Do: If Β¬(P i), break. i := i + 1. Loop. γ)
23:35:55 <fax> hi oklookpaoufpadda
23:36:02 <fax> I got something to show you
23:36:14 <fax> www.stanford.edu/~dgleich/publications/finite-calculus.pdf !
23:36:24 <fax> you said you didn't like analysis because it wasn't finite enough
23:38:09 <oklokok> well i'm not sure that's exactly that i said :D
23:38:12 <Wareya> http://i43.tinypic.com/2v8s9w8.png
23:38:16 <alise_> I see fax doesn't like my proof :(
23:38:19 <fax> oklokok this stuff is so cool though!
23:38:20 <Wareya> 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
23:38:22 <fax> seriously I have to master it
23:38:23 <Wareya> Dude: and what is that, what is it made of?
23:38:26 <Wareya> Scientist: Really we have no fucking clue, we hoped you'd stop asking after hearing "dark energy"
23:38:35 <fax> alise: I just assumed it was correct
23:38:52 <alise_> yet another lol-they-call-it-dark-it-must-just-be-made-up bullshit story
23:38:59 <alise_> be ignorant elsewhere :|
23:39:35 <alise_> decide on the reals is interesting btw
23:39:39 <alise_> nested halting-checking
23:40:47 <alise_> [Note to the editor: Insert a "your mom" joke here.]
23:46:29 <alise_> 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
23:50:34 <fax> oklopkoupuo i think this is a precursor to Umbral Calculus
23:50:52 <fax> not entirely sure
23:53:11 <fax> oklokok btw I have not done OR yet :(
23:53:28 <fax> actually I was going to try and code that stuff into epigram just for fun but it was too hard
23:53:43 <fax> (I couldn't even define a tree type)
23:53:54 <cpressey> alise_, what did you think of my proof?
23:53:58 <oklokok> you can ask for hints if you want
23:54:15 <alise_> cpressey: which proof?
23:54:16 <fax> oklokok, well if you had an intermediate problem between AND and OR that would be good :p
23:54:48 <cpressey> It's wrong. The last thing on the 3rd line should be "Stack'"
23:55:05 <alise_> cpressey: You've neglected to specify what you're proving, for starters.
23:55:18 <alise_> Looks more like an evaluation to me,
23:55:43 <cpressey> Theorem is always: first line and last line of "proof" section are equal.
23:55:55 <alise_> cpressey: That's a rubbish proof system
23:55:56 <cpressey> What is a proof if not an evaluation?
23:55:56 <fax> Gian-Carlo Rota began his career as a functional analyst, but changed directions and became a distinguished combinatorialist. -- he helped develop this umbral calculus
23:55:59 <oklokok> for most things that are in the middle, you'll need to have OR already
23:56:02 <alise_> cpressey: A proof is a value
23:56:18 <alise_> fax: link to that book that had tons of proofs in i think coq
23:56:18 <cpressey> Well, sure, everything is a value
23:56:18 <oklokok> if you can live with using OR before knowing how to compile it, then yeah i have a few
23:56:21 <alise_> supposedly from the future
23:56:27 <alise_> cpressey: No, quite literally
23:56:34 <alise_> p : P where P : Prop = p is a proof of P
23:57:01 <fax> oklokok oh, I was thinking about AxB = BxA, it seems to only have solutions like A = (mnux)^n(mnu), B = ..^m...
23:57:02 <alise_> there's a reason proof assistants are all dependent and whatnot, it's because this is the way things make sense in computing
23:57:27 <fax> alise, I don't know what you are referring to
23:57:38 <fax> not all proof assistants work on dependent type theory
23:57:53 <fax> but dependent type theory is really an excellent way to do it imo
23:58:13 <oklokok> if |A|>|B|, then TxB = xBT, which gives you all the solutions
23:58:31 <fax> oklokok huh??
23:58:33 <oklokok> there are a few basic techniques that get you through most things
23:58:41 <alise_> but are all-dependent-and-whatnot
23:58:50 <oklokok> fax: i just substituted A = BT because |A| > |B|
23:58:59 <oklokok> there's a symmetric case for B > A
23:59:17 <oklokok> oh and after that you already have all the solutions
23:59:25 <oklokok> if you don't see it... see fundamental theorem
23:59:35 <cpressey> 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.
23:59:46 <oklokok> we should probably be doing this in pm, i'm not sure it's as entertaining to others
23:59:49 <cpressey> And since a proof is a series of derivations, I don't see anything wrong with this.
23:59:59 <oklokok> we should be doing this tomorrow