00:00:45 <Sgeo> Smalltalk at: #One put: 1.
00:09:00 -!- augur has joined.
00:10:39 <Sgeo> Smalltalk globals keysAndValuesDo: [:key :value |
00:10:39 <Sgeo> (value class class = Metaclass) ifFalse: [
00:10:39 <Sgeo> Transcript cr.
00:10:39 <Sgeo> Transcript show: key]]
00:10:54 <Sgeo> May have some false positives
00:14:29 <tswett> In my image, there are 16.
00:15:12 <Sgeo> I seem to have many more than 16
00:15:26 <tswett> Some of them are traits.
00:15:29 <tswett> Which are like classes.
00:15:35 -!- sftp has quit (Remote host closed the connection).
00:15:38 -!- sftp_ has joined.
00:16:10 <tswett> Optimist, Sensor, SystemOrganization, World, Display, ActiveEvent, TextConstants, Smalltalk, Processor, ScheduledControllers, Transcript, SourceFiles, ActiveHand, ActiveWorld, Undeclared, ImageImports.
00:16:43 <Sgeo> I don't have Optimist
00:16:52 <tswett> Optimist is strange. It's a True.
00:17:40 -!- fungot has quit (Read error: Operation timed out).
00:18:46 -!- fizzie has quit (Ping timeout: 248 seconds).
00:21:28 -!- fizzie has joined.
00:35:15 <Vorpal> <Sgeo> ActiveWorld! <-- different one I suspect
00:35:54 <Vorpal> <tswett> Optimist is strange. It's a True. <-- Pessimist should be False then?
00:37:50 <tswett> It should be, but it isn't.
00:57:14 <Sgeo> So, what uses Optimist?
00:57:19 <Sgeo> Is it possible to determine?
01:10:14 <tswett> I don't know of any way to determine that. You could look through all of the code in the system and see if it uses Optimist.
01:10:43 <tswett> Or you could replace Optimist with an object that pretends to be true but logs all its accesses.
01:11:28 <Sgeo> tvvl: Smalltalk globals remove: #Smalltalk
01:11:47 <tswett> No worries, this bot is supposed to be abused.
01:11:50 <Sgeo> I'm sure I had something more creative in mind
01:11:53 <tswett> It's not *made* to be abused, but it's supposed to be. :P
01:12:13 <tswett> It looks like that expression is simply an error.
01:12:22 <tswett> The image is still working perfectly.
01:12:45 <tswett> I suggest "Smalltalk globals at: #Smalltalk put: nil".
01:12:47 -!- tswettbot-boxed- has joined.
01:13:01 <tswett> I'll see what that does.
01:13:03 <tswett> tvvl: Smalltalk globals at: #Smalltalk put: nil
01:13:12 -!- tswettbot-boxed has quit (Remote host closed the connection).
01:13:28 <tswett> There. *Now* the image has crashed.
01:14:06 -!- tswettbot-boxed- has quit (Remote host closed the connection).
01:15:00 -!- tswettbot-boxed has joined.
01:15:01 <tswett> Feel free to repair the bot through IRC. :P
01:15:17 <tswett> You just need to fix a certain method.
01:16:10 <tswett> tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) methodSourceString
01:16:22 <tswett> Oh, that's not how that works.
01:16:27 <tswett> I dismiss you, tswettbot.
01:16:35 -!- tswettbot-boxed has quit (Remote host closed the connection).
01:16:51 -!- tswettbot-boxed- has joined.
01:17:08 <tswett> tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource
01:17:27 <tswett> Of course it sends every line of that as a separate IRC command.
01:18:00 <tswett> Yep, that's the name of the project.
01:19:58 <tswett> tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource withBlanksCondensed
01:22:58 <tswett> tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource onlyLetters
01:22:58 <tswettbot-boxed-> bottheardtttTranscriptshowRCVDtcrtbeginsWithPINGifTruetsendMessagePONGtincludesSubStringIdismissyoutswettbotifTruetquitttvvlttfindStringttifFalsetsendMessagePRIVMSGesotericCompilerevaluatetallButFirsttsizetnotifyingnilloggedfalseasString
01:24:59 <tswett> tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource select: [:x | x ~= Character cr and: [x ~= Character lf]]
01:25:00 <tswettbot-boxed-> bot: t1 heard: t2 | t3 t4 |Transcript show: 'RCVD: ' , t2; cr.(t2 beginsWith: 'PING')ifTrue: [t1 sendMessage: 'PONG'].(t2 includesSubString: 'I dismiss you, tswettbot')ifTrue: [t1 quit].t3 := 'tvvl: '.t4 := t2 findString: t3.t4 = 0ifFalse: [t1 sendMessage: 'PRIVMSG #esoteric :' , (Compilerevaluate: (t2 allButFirst: t3 size + t4 - 1)notifying: nillogged: false) asString]
01:27:35 <tswett> tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource select: [:x | ({Character cr. Character lf. Character tab} includes: x) not]
01:27:35 <tswettbot-boxed-> bot: t1 heard: t2 | t3 t4 |Transcript show: 'RCVD: ' , t2; cr.(t2 beginsWith: 'PING')ifTrue: [t1 sendMessage: 'PONG'].(t2 includesSubString: 'I dismiss you, tswettbot')ifTrue: [t1 quit].t3 := 'tvvl: '.t4 := t2 findString: t3.t4 = 0ifFalse: [t1 sendMessage: 'PRIVMSG #esoteric :' , (Compilerevaluate: (t2 allButFirst: t3 size + t4 - 1)notifying: nillogged: false) asString]
01:27:44 <tswett> There, there's your source code. :P
01:28:26 <tswett> Oh, interesting. All the argument names are absent.
01:29:13 <tswett> All the argument names in the entire image. And there are no comments.
01:29:24 <tswett> I'm guessing that's supposed to happen when the sources file can't be found.
01:37:52 -!- lament has joined.
01:52:13 <tswett> coppro: I know, i know.
02:03:06 -!- augur has quit (*.net *.split).
02:03:06 -!- Zuu has quit (*.net *.split).
02:03:06 -!- variable has quit (*.net *.split).
02:03:06 -!- Ilari has quit (*.net *.split).
02:03:06 -!- Ilari_antrcomp has quit (*.net *.split).
02:03:06 -!- tswettbot-boxed- has quit (*.net *.split).
02:03:06 -!- fizzie has quit (*.net *.split).
02:03:06 -!- R-Type has quit (*.net *.split).
02:03:06 -!- jix has quit (*.net *.split).
02:03:06 -!- Slereah has quit (*.net *.split).
02:03:06 -!- aloril has quit (*.net *.split).
02:03:06 -!- bsmntbombdood has quit (*.net *.split).
02:03:06 -!- Zwaarddijk has quit (*.net *.split).
02:03:06 -!- dbc has quit (*.net *.split).
02:03:06 -!- comex has quit (*.net *.split).
02:03:06 -!- marchdown has quit (*.net *.split).
02:03:06 -!- coppro has quit (*.net *.split).
02:03:06 -!- nooga_ has quit (*.net *.split).
02:03:06 -!- olsner has quit (*.net *.split).
02:03:06 -!- yiyus has quit (*.net *.split).
02:03:06 -!- sebbu2 has quit (*.net *.split).
02:03:06 -!- z^ck has quit (*.net *.split).
02:03:06 -!- lifthras1ir has quit (*.net *.split).
02:03:06 -!- sftp_ has quit (*.net *.split).
02:03:06 -!- wareya_ has quit (*.net *.split).
02:03:06 -!- Wamanuz4 has quit (*.net *.split).
02:03:06 -!- jcp has quit (*.net *.split).
02:03:06 -!- EgoBot has quit (*.net *.split).
02:03:06 -!- lambdabot has quit (*.net *.split).
02:03:06 -!- Gregor has quit (*.net *.split).
02:03:06 -!- clog has quit (*.net *.split).
02:03:06 -!- Deewiant has quit (*.net *.split).
02:03:06 -!- lament has quit (*.net *.split).
02:03:06 -!- azaq23 has quit (*.net *.split).
02:03:06 -!- Lymia has quit (*.net *.split).
02:03:06 -!- tswett has quit (*.net *.split).
02:03:06 -!- Vorpal has quit (*.net *.split).
02:03:06 -!- pingveno has quit (*.net *.split).
02:03:06 -!- HackEgo has quit (*.net *.split).
02:03:06 -!- yorick has quit (*.net *.split).
02:03:06 -!- copumpkin has quit (*.net *.split).
02:03:06 -!- shachaf has quit (*.net *.split).
02:03:06 -!- oklopol has quit (*.net *.split).
02:03:06 -!- ineiros has quit (*.net *.split).
02:03:06 -!- SimonRC has quit (*.net *.split).
02:03:06 -!- mtve has quit (*.net *.split).
02:03:06 -!- cheater00 has quit (*.net *.split).
02:03:06 -!- Sgeo has quit (*.net *.split).
02:03:06 -!- Mannerisky has quit (*.net *.split).
02:03:06 -!- quintopia has quit (*.net *.split).
02:03:06 -!- nottwo has quit (*.net *.split).
02:03:06 -!- enki-[quit] has quit (*.net *.split).
02:03:36 -!- glogbackup has joined.
02:03:36 -!- Katovatzschyn has joined.
02:03:36 -!- lament has joined.
02:03:36 -!- tswettbot-boxed- has joined.
02:03:36 -!- fizzie has joined.
02:03:36 -!- sftp_ has joined.
02:03:36 -!- augur has joined.
02:03:36 -!- cheater00 has joined.
02:03:36 -!- Sgeo has joined.
02:03:36 -!- sebbu2 has joined.
02:03:36 -!- R-Type has joined.
02:03:36 -!- copumpkin has joined.
02:03:36 -!- enki-[quit] has joined.
02:03:36 -!- marchdown has joined.
02:03:36 -!- wareya_ has joined.
02:03:36 -!- Zuu has joined.
02:03:36 -!- azaq23 has joined.
02:03:36 -!- Lymia has joined.
02:03:36 -!- coppro has joined.
02:03:36 -!- z^ck has joined.
02:03:36 -!- quintopia has joined.
02:03:36 -!- nottwo has joined.
02:03:36 -!- jix has joined.
02:03:36 -!- EgoBot has joined.
02:03:36 -!- variable has joined.
02:03:36 -!- tswett has joined.
02:03:36 -!- Ilari has joined.
02:03:36 -!- Ilari_antrcomp has joined.
02:03:36 -!- Vorpal has joined.
02:03:36 -!- nooga_ has joined.
02:03:36 -!- SimonRC has joined.
02:03:36 -!- lifthras1ir has joined.
02:03:36 -!- olsner has joined.
02:03:36 -!- yiyus has joined.
02:03:36 -!- Wamanuz4 has joined.
02:03:36 -!- lambdabot has joined.
02:03:36 -!- Gregor has joined.
02:03:36 -!- shachaf has joined.
02:03:36 -!- clog has joined.
02:03:36 -!- Deewiant has joined.
02:03:36 -!- jcp has joined.
02:03:36 -!- mtve has joined.
02:03:36 -!- pingveno has joined.
02:03:36 -!- oklopol has joined.
02:03:36 -!- ineiros has joined.
02:03:36 -!- HackEgo has joined.
02:03:36 -!- yorick has joined.
02:03:40 -!- glogbackup has left.
02:03:57 -!- rodgort` has quit (Ping timeout: 240 seconds).
02:04:06 -!- comex has joined.
02:04:09 -!- Slereah has joined.
02:04:09 -!- aloril has joined.
02:04:09 -!- bsmntbombdood has joined.
02:04:09 -!- Zwaarddijk has joined.
02:04:09 -!- dbc has joined.
02:04:19 -!- Katovatzschyn has quit (Remote host closed the connection).
02:04:30 -!- augur has quit (Remote host closed the connection).
02:09:20 -!- rodgort has joined.
02:10:41 -!- azaq23 has quit (Quit: Leaving.).
02:12:00 -!- tswettbot-boxed- has quit (Read error: Operation timed out).
02:22:37 -!- copumpkin has quit (Ping timeout: 246 seconds).
02:23:17 -!- copumpkin has joined.
02:27:33 -!- augur has joined.
02:43:25 <oklopol> augur: you always join but never leave, how is that possible
02:49:44 -!- lament has quit (Ping timeout: 248 seconds).
02:51:14 <oklopol> augur: i've just never noticed you leave
02:51:24 <augur> you're not paying attention then!
02:51:26 <oklopol> yay complexity theory has been discussed here
02:51:51 <oklopol> oh i thought you had done some sorta magix
02:52:37 <oklopol> if there are sparse NP-complete sets with respect to many-to-one reductions, then P=NP, same for sparse coNP-complete sets
02:53:22 <oklopol> sparse = for some polynomial p there are at most p(n) words of length n in the language
02:54:56 <Zwaarddijk> oklopol: even worse, if there's unary languages that are NP-complete, P=NP
02:55:16 <oklopol> Zwaarddijk: i'm actually just now writing the proof of that
02:56:13 <oklopol> easy one: if there's a tally set (subset of 1^*) that's NP-complete, then P=NP: take an SAT instance, and one var at a time branch to both the true and the false case, now just note the set of formulas you get never gets exponential because you can prune out two formulas if they have the same image in the tally set
02:56:25 <oklopol> yes i was writing it for your pleasure
02:56:36 <oklopol> but that was kinda simplified
02:56:43 <oklopol> i'll be happy to get into the details ofc
02:57:56 <oklopol> you need an SAT encoding where setting a value to true or false doesn't increase its length
02:58:22 <oklopol> then let p be a polynomial such that the reduction from SAT to the tally set takes time at most p
02:59:05 <oklopol> and note that if the SAT instance has size n, then the images of all formulas you get when branching are at most size p(n)
02:59:53 <oklopol> and in fact there are at most p(n) formulas you need to keep track of, because for all formulas, you can remove them if they don't have an image in 1^*, and if they do have an image in 1^*, it's at most length p(n), and for each length, you store just one formula
03:00:29 <oklopol> that should be the key points
03:01:00 <oklopol> kind of a random list of facts
03:01:45 <Zwaarddijk> I was thinking, btw, how would a language like
03:02:19 <Zwaarddijk> 1^(R(x,y), x and y being any integer, and R() being the Ramsey numbers
03:02:45 <Zwaarddijk> R(x,y) is very difficult to compute, but is that even relevant to the language itself?
03:03:33 <oklopol> i'm sure no one knows a fast algorithm for that because R(5,5) is open
03:03:47 <Zwaarddijk> does this mean that language is difficult
03:03:50 <augur> oklopol: ever played with agda?
03:04:53 <oklopol> Zwaarddijk: even though tally sets cannot be NP-complete, they can be exponential time or even uncomputable
03:05:16 <oklopol> there was something about NP-hardness
03:05:29 <oklopol> oh well we certainly know they can be uncomputable
03:05:52 <Zwaarddijk> well, the NP-completeness is unknown, that was my point
03:06:18 <Zwaarddijk> does P=NP => NP-complete tally sets, or is it just NP-complete tally sets => P=NP?
03:06:35 <oklopol> if P=NP, then {1} is MP-complete
03:07:25 <oklopol> but my ct books says tally sets cannot be even bounded truth table hard for NP
03:07:43 <oklopol> i guess that's essentially the same thing
03:08:08 <Zwaarddijk> when I read the thing about tally sets first
03:08:15 <Zwaarddijk> I figured that's pretty much proof that P!=NP
03:08:46 <Zwaarddijk> or maybe at least the closest we have?
03:09:04 <oklopol> erm the reason i gave the proof is that it's a simple little thingie
03:09:25 <oklopol> sparse NP-complete => P=NP is much more interesting
03:10:29 <oklopol> and i don't understand it. i have understood the details separately, once upon a time, but i'm not sure i ever really got what the idea was
03:11:03 <oklopol> sparse coNP-complete => P=NP is essentially the same as that tally set proof, but i don't recall how it goes, similar pruning thing
03:11:17 <augur> oklopol: you should
03:12:08 <oklopol> but umm, i should go to work
03:12:38 <Zwaarddijk> I have recently realized I should learn javascript :|
03:18:36 <Zwaarddijk> yes, it is a terrible thing to realize
03:23:46 <Gregor> http://sss.cs.purdue.edu/projects/dynjs/javascript_the_evil_parts.png <-- recommended book to learn from
03:29:46 <augur> oklopol: you do math, right?
03:30:41 <Gregor> augur: I don't do math :P
03:30:51 <augur> im just saying hi to you
03:31:01 <Gregor> No, you're saying "Gregor!" to me.
03:31:20 -!- copumpkin has quit (Quit: Computer has gone to sleep.).
03:31:52 <augur> Gregor: yes, thats a way of saying hi
03:31:56 <augur> oklopol: well, you can do math in agda!
03:32:04 <augur> for instance, im doing abstract algebra right now!
03:32:11 <Gregor> You can do math in JavaScript too X-P
03:32:16 <augur> Gregor: i mean proofs
03:32:17 <oklopol> what's abstract algebra, is it universal algebra?
03:32:27 <Gregor> augur: And I mean to trollolol :P
03:32:36 <augur> oklopol: eh. in this case its just some graph-theoretic stuff i guess?
03:33:19 <oklopol> must be pretty damn abstract if you don't know what it is
03:34:16 <oklopol> according to wp, abstract algebra is the same as universal algebra
03:34:24 <Gregor> augur: I didn't get libc.so *sobblecopter*
03:34:47 -!- sebbu has joined.
03:35:28 <Gregor> augur: Why even say "hi" if I can't then relate personal tragedy :P
03:35:30 <oklopol> i imagine doing math in agda would be similar to programming in brainfuck, sure it can be fun but you'll be proving 1+1=2.
03:37:29 <augur> currently im proving that any graph order built from Unit and disjunctive concatenation will be a linear order
03:37:42 <oklopol> disjunctive concatenation?
03:38:56 -!- sebbu2 has quit (Ping timeout: 276 seconds).
03:38:57 <augur> concatenation with disjoint union of the underlying sets
03:39:20 <oklopol> and how do you "concatenate" graphs
03:39:37 <augur> in this case, its roughly like so
03:41:38 <augur> (X, arrX) ++ (Y, arrY) = (X + Y, \(z,z') -> if z z' <- X then arrX z z' else if z <- X & z' <- Y then true else if z <- Y & z' <- X then false else if z z' <- Y then arrY z z')
03:41:58 <augur> plus the relevant isomorphism to make the new relation be of type (X + Y) x (X + Y) -> Bool
03:42:12 <oklopol> so connect vertices of X to those of Y
03:42:27 <augur> right, the X's point to the Y's
03:42:39 <oklopol> well obviously that's a total order
03:42:48 <augur> the X's dont point to themselves
03:42:52 <augur> total orders are reflexive
03:42:58 <augur> linear orders are irreflexive
03:43:04 <augur> i mean, it COULD be total
03:43:25 <augur> depending on whether you state from (1, const True) or (1, const False)
03:43:34 <augur> the former is a total order, the latter is a linear order
03:43:40 <oklopol> well okay linear, point is that's obvious, easier than 1+1=2
03:43:58 <augur> perhaps! depends on how you define 1, 2, and + :)
03:44:11 <augur> but its neat cause ive got a _proof_
03:44:25 <augur> im still constructing the proof that (1, const False) is a linear order
03:44:30 <oklopol> it's NEAT, but it's not math
03:44:43 <oklopol> well it's math but it's kidss math
03:45:35 <augur> but you can do growed up math too!
03:45:39 <augur> im just not doing that kind of math
03:45:45 <augur> because its not relevant to my work
03:45:48 <oklopol> doing math is all about the basic idea, formal proof is a lot of fun, but it's not really why i'm into math
03:46:21 <oklopol> i'm on a course about formal proving
03:46:57 <oklopol> hopefully i'll be able to prove that same theorem in a month or so
04:03:10 -!- copumpkin has joined.
04:10:41 -!- augur_ has joined.
04:11:43 -!- augur has quit (Read error: Connection reset by peer).
04:25:55 -!- augur_ has quit (Read error: Connection reset by peer).
04:25:57 -!- augur has joined.
04:43:48 -!- asiekierka has joined.
05:05:12 -!- copumpkin has changed nick to wharrrgarbl.
05:12:57 -!- asiekierka has quit (Ping timeout: 240 seconds).
05:17:33 -!- sftp_ has quit (Remote host closed the connection).
05:27:52 -!- augur has quit (Remote host closed the connection).
05:29:24 -!- augur has joined.
05:38:37 -!- lifthrasiir has joined.
05:38:37 -!- fizzie has quit (Ping timeout: 264 seconds).
05:38:42 -!- fizzie has joined.
05:43:05 -!- lifthras1ir has quit (Ping timeout: 276 seconds).
06:03:33 -!- aloril has quit (Ping timeout: 240 seconds).
06:16:26 -!- aloril has joined.
06:49:04 -!- Lymia has quit (Read error: Connection reset by peer).
06:50:39 -!- Lymia has joined.
06:50:39 -!- Lymia has quit (Changing host).
06:50:39 -!- Lymia has joined.
07:25:23 -!- lament has joined.
07:29:12 -!- oerjan has joined.
07:52:33 -!- cheater99 has joined.
07:53:29 -!- cheater00 has quit (Ping timeout: 246 seconds).
08:34:44 <fizzie> Newsgroups: sci.math,comp.theory,sci.logic,comp.lang.c,alt.religion.christianity
08:34:44 <fizzie> Subject: Alpha and Omega R-Language Computer Code|Robot Jesus|Sermon on the Mount|
08:35:09 -!- lament has quit (Ping timeout: 276 seconds).
08:57:33 <mtve> quite esoteric - http://arxiv.org/abs/1104.0924v1
09:08:36 -!- oerjan has quit (Quit: leaving).
09:30:16 <Vorpal> <fizzie> Newsgroups: sci.math,comp.theory,sci.logic,comp.lang.c,alt.religion.christianity <-- that's a joke, right?
09:31:04 <Vorpal> fizzie, or was that not a To list for one message?
09:31:30 <fizzie> There's no "To:" header in postings; but it was a Newsgroups: header for one (crossposted) message, yes.
09:31:59 <fizzie> I mean, it does have both "computer code" and "robot jesus" in the subject, why not.
09:32:57 <fizzie> The contents didn't really make sense, though: http://groups.google.com/group/comp.lang.c/msg/5e1c4335efdc2ecf
09:42:39 <Vorpal> fizzie, looks like program code
09:42:52 <Vorpal> fizzie, probably in R as it said in the subject
09:43:01 <fizzie> The syntax looks like R, yes.
09:43:09 <fizzie> Well, except those quotation bits.
09:43:11 <Vorpal> I don't know R however.
09:43:31 <Vorpal> fizzie, could be some sort of comment? I don't know
09:43:41 <fizzie> I'm not an R expert either, but I doubt "be comforted by the words which I give unto" is valid syntax.
09:44:02 <Vorpal> it could be doing the intercal way. Invalid syntax = comment
09:44:15 <fizzie> R comments are from # to end-of-line.
09:46:07 <fizzie> The same author posted a P=NP "proof" the other day, too.
10:03:58 -!- nooga_ has quit (Remote host closed the connection).
10:20:39 -!- BeholdMyGlory has joined.
10:20:47 -!- augur has quit (Read error: Connection reset by peer).
10:21:07 -!- augur has joined.
10:25:01 -!- augur has quit (Read error: Connection reset by peer).
10:25:20 -!- augur has joined.
10:33:04 -!- lmk0tter has joined.
10:33:12 -!- Imk0tter has joined.
10:34:31 -!- lmk0tter has quit (Client Quit).
10:37:40 -!- Imk0tter has quit.
10:37:59 -!- Imk0tter has joined.
10:55:10 -!- Lymia_ has joined.
10:55:15 -!- Lymia has quit (Read error: Connection reset by peer).
11:46:14 -!- k0tk0t has joined.
11:46:21 -!- PatashuNuMou has joined.
11:47:10 <k0tk0t> ,[->+>+<<]>>[<<+>>-]>+>>++++++[<<[>++<-]>[<+++++>-]>-]<<[->+>+<<]>>[<<+>>-]>>+<<<<[>>>>>>>>>>>[-]+[<<<<<<<<<<<<<[->>>>>>>>+<<<<<<<<]>>>[->>>>>>+<<<<<<]<[->+>+<<]>>[<<+>>-]>>>>[>[-<->>>+<]<<]<[>]>[-<<<<<<<<+>>>>>>>>]>[-]>>>+<[-<<<<<<<<->>>>>>>>]<<<<<<<<[[-]>>>>>>>>>->-<<<<<<<<<<]<[->+>+<<]>>[<<+>>-]>>>>>>>>>]<[->>+>+<<<]++++++[->>++++++++<<]>>.[-]>[-<<<<<<<<<<<<[-]<[->+>+<<]>>[<<+>>-]<[->>>>>>>>>>>>>+<<<<<<<<<<<<<]>>>>>>>>>>>>]>[
11:51:02 -!- wth has joined.
11:51:04 -!- wth has quit (Remote host closed the connection).
11:53:12 -!- k0tk0t has quit (Remote host closed the connection).
11:53:34 -!- k0tk0t has joined.
11:55:31 -!- fungot has joined.
11:58:21 <k0tk0t> anyone familiar with brainfuck?
11:59:19 -!- k0tk0t has quit (Quit: k0tk0t).
11:59:53 -!- wth has joined.
12:02:16 -!- wth has left.
12:02:49 <Vorpal> <k0tk0t> anyone familiar with brainfuck? <-- yes, to some degree
12:04:09 <Vorpal> hm, I think bf is one of the few languages where output of a good optimising compiler might be easier to follow than the original source code for most programs.
12:04:46 <Vorpal> (of course it is probably possible to obfuscate code in many languages to get that effect there too)
12:06:46 <Vorpal> well, probably the same goes for some other easily compileable tarpits
12:08:39 -!- wth has joined.
12:11:31 -!- BeholdMyGlory has quit (Remote host closed the connection).
12:14:00 -!- BeholdMyGlory has joined.
12:24:50 -!- FireFly has joined.
12:32:10 <Ilari> Hah. I seemingly got signed up to one mailing list in "opt-out" fashion (quite understandable given the situation).
12:32:22 -!- sftp has joined.
12:32:38 <Vorpal> Ilari, what mailing list heh?
12:33:27 <Ilari> Well, basically one mailing list was shut down and new one created to continue (apparently mailman can't rename mailing lists).
12:33:46 <Vorpal> well that makes sense then
12:33:50 <Ilari> And the admins copied the subscriber lists.
12:33:54 <Vorpal> (well, mailmail doesn't)
12:34:33 <Ilari> All data wasn't copied. The password changed for instance.
12:36:35 -!- wth has left ("Leaving.").
12:59:16 -!- Wamanuz4 has quit (Read error: Operation timed out).
13:00:00 -!- jcp has quit (Read error: Operation timed out).
13:01:23 -!- Wamanuz4 has joined.
13:06:45 -!- wharrrgarbl has quit (Quit: Computer has gone to sleep.).
13:07:58 -!- jcp has joined.
13:09:49 -!- PatashuNuMou has quit (Quit: MSN: Patashu@hotmail.com , Gmail: Patashu0@gmail.com , AIM: Patashu0 , YIM: patashu2 .).
13:14:58 -!- augur has quit (Remote host closed the connection).
13:27:25 -!- asiekierka has joined.
13:29:12 -!- wharrrgarbl has joined.
13:44:42 -!- augur has joined.
14:14:27 -!- cheater00 has joined.
14:15:21 -!- cheater99 has quit (Ping timeout: 246 seconds).
14:28:54 -!- Slereah has quit (Ping timeout: 240 seconds).
14:35:23 -!- cpressey has joined.
14:35:51 -!- Slereah has joined.
14:36:25 <cpressey> R-Type! You survived the night!
14:39:09 -!- Sgeo has quit (Ping timeout: 246 seconds).
14:43:18 -!- wareya_ has changed nick to wareya.
14:54:48 <Vorpal> cpressey, hm, why did you make the bot act like that? Is it a reference I'm missing or something?
15:01:55 <cpressey> Vorpal: Well: I wanted to write a bot in R, just because R is a horrible language to do such a thing in. I named it 'R-Type' because 'rbot' was taken, 'R-bot' is boring, and R-Type was a significant game in the history of video games (not a huge favorite of mine, but I can appreciate it.) Since the point was just to write a bot in R, I didn't care what it actually did. So I modelled its personality after a cat I met o
15:02:33 <Vorpal> cpressey, I think that got cut off
15:02:39 <Vorpal> "So I modelled its personality after a cat I met o"
15:02:49 <cpressey> So I modelled its personality after a cat I met once.
15:03:03 <Vorpal> I guess a rather annoying cat...
15:04:08 <cpressey> It was a stray that was rescued. It was also a longhair.
15:04:46 <cpressey> Longhair + living on the streets = permanent knots in fur = quite painful, I imagine = not the happiest individual.
15:04:47 -!- pumpkin has joined.
15:06:06 <cpressey> Oh, I should post its source code somewhere so you can bask in the glory
15:06:39 -!- wharrrgarbl has quit (Ping timeout: 276 seconds).
15:08:00 <Vorpal> cpressey, I don't know R though
15:08:02 -!- Phantom_Hoover has joined.
15:09:47 <cpressey> Vorpal: you don't have to know it to appreciate how BEAUTIFUL it is.
15:10:02 <cpressey> See the beauty! http://pastie.org/1768075
15:10:43 <cpressey> The command line to run it, alone, is worth it.
15:11:00 <Gregor> "irc.irc.irc" is the greatest hostname ever.
15:11:28 <Vorpal> cpressey, if you want to avoid the erlang shell you can get pretty silly command lines there too
15:12:23 <Phantom_Hoover> "Every time I hear that XKCD isn't funny anymore I get slightly pissed off. It's always been hit and miss but the hits so outweigh the misses that it's my favourite on line comic (with the possible exception of Doonesbury)." ← a decent precis of why I left RationalWiki.
15:13:05 <Phantom_Hoover> "I am continually impressed/annoyed that we spent zillions of edits and hundreds of words making a point in favour of rationalism, then XKCD kicks our arses saying the same thing in four panels with a couple of matchstick men."
15:14:21 <Vorpal> Phantom_Hoover, hm I'd say xkcd is sometimes good, though rather rarely nowdays. And even back in the "good old days" it wasn't always good.
15:15:47 <Phantom_Hoover> the master xkcd will rise from the sunken city of frwgll
15:15:51 <cpressey> I know as much about xkcd as I want to -- more, actually. I should not tempt fate. Or #esoteric.
15:16:50 <Vorpal> cpressey, I'm not sure if you meant you didn't know what xkcd was above or not. It is however a webcomic.
15:17:11 <oklopol> http://www.xkcd.com/879/ <<< i like this one
15:17:49 -!- pumpkin has changed nick to wharrrgarbl.
15:18:05 <oklopol> http://www.xkcd.com/881/ <<< and could someone explain this to me
15:18:12 <cpressey> Vorpal: Depending on who you ask, it is THE webcomic.
15:18:18 <oklopol> is the joke that they have a weird way of hugging
15:20:20 <oklopol> but i suppose it's still the simpsons of webcomics
15:21:28 <oklopol> err... sure? now can you explain 881 to me
15:22:32 <Phantom_Hoover> It's about LOOK AT ME I CAN WRITE CRINGEWORTHILY AWFUL "EMOTIONAL" COMICS WITH SCIENCE SHOEHORNED IN I AM NERD HUMOUR
15:22:55 <cpressey> I am fascinatingly tempted to actually look at it.
15:23:12 <Phantom_Hoover> Also *anyone* who thinks probability is worth doing for practical applications should be shot.
15:23:28 <oklopol> are you sure there isn't some sort of punchline?
15:23:43 <oklopol> what are the numbers in the table
15:23:51 <Phantom_Hoover> The impression I get is that the actual *mathematics* requires some kind of degree.
15:24:10 <oklopol> like, that many survive 5/10 years of X
15:25:03 <oklopol> and i wonder if the way they hug is relevant
15:25:57 <oklopol> i think i just don't get it
15:26:05 <cpressey> Perhaps if I prepare myself mentally and emotionally beforehand sufficiently, I can look at it.
15:26:19 <oklopol> cpressey: i would appreciate that
15:26:36 <cpressey> I mean, I have seen xkcd's involuntarily on peoples' shirts and hanging in their cubes, and it didn't damage me *too* much.
15:26:40 <oklopol> fun little problem: find a 5-regular planar graph, where 5-regular = every vertex has degree 5
15:26:43 <Phantom_Hoover> oklopol, I think you're assuming there's an actual joke somewhere under the mawkish sentimentalism, and are combing through it.
15:28:00 <cpressey> Phantom_Hoover: You are correct in that.
15:28:23 <Phantom_Hoover> Well, unless you have the love for your fellow humans of Charlie Brooker.
15:28:56 <cpressey> I don't know who that is and the extra information is not helping me recover.
15:29:16 <Phantom_Hoover> Charlie Brooker is an infamously misanthropic reviewer of things.
15:29:21 <oklopol> i suppose this is the right time to tell cpressey that santa isn't real
15:29:28 <cpressey> OK, well: oklopol, if you want my opinion: it wasn't intended to be funny.
15:29:47 <cpressey> It was intended to be Hallmark-y.
15:30:02 <cpressey> For lack of a better adjective.
15:30:15 -!- impomatic has joined.
15:30:54 <cpressey> "mawkish sentamentalism", I suppose that's a good way to put it too
15:33:05 <cpressey> oklopol: this was all a PLOT by you, to get me to read an xkcd, WASN'T IT
15:33:29 <cpressey> cleverly FEIGNING non-understanding of the fail
15:33:51 <cpressey> hm, or can you actually call that fail? because i'm sure it was totally what was intended
15:34:13 <oklopol> i wouldn't know, I DON'T GET IT
15:34:19 <cpressey> oklopol: THERE IS NOTHING TO GET
15:34:58 <cpressey> oklopol: Are you familiar with a pre-web comic strip called Fred Bassett?
15:35:31 <cpressey> Sometimes, there is nothing to get.
15:35:33 <oklopol> no, except if it's pre-web i might know it in finnish
15:36:24 <cpressey> (the internet is amazing sometimes)
15:37:16 <oklopol> oh yeah i've seen those comics
15:37:40 <cpressey> "Some strips are merely a surreal or whimsical description of a moment of life as seen from a dog's point of view. As very British cartoon strips, they break the normal strip rules by sometimes not having a traditional ending, a punchline or even a distinct purpose, distinguishing them from the more direct, American-style Garfield or Peanuts strips."
15:39:47 <oklopol> maybe i'll try to solve it tomorrow
15:40:02 <oklopol> koiraskoira sounds really silly
15:40:22 <cpressey> I mean, I always thought it must be hard being a comic strip writer, you have to come up with a new funny thing for every day. But! Not if you aren't actually funny every day.
15:41:05 <oklopol> well you can always just make a play on words
15:41:27 <oklopol> never funny, but good enough for a newspaper comic strip.
15:42:14 <cpressey> I have this particular strip hanging in my cube: http://www.glyphjockey.com/uploaded_images/Uncanny_Old_Gags_1-772109.jpg
15:42:34 <cpressey> It's revenge against those who see fit to hang xkcds where others can see them.
15:43:15 <oklopol> i.... don't get that one either
15:43:23 <oklopol> have i become even stupider
15:45:51 <oklopol> is the points that bad things can happen even though no actual failing is involved, proper walking can cause footprints in the wrong place, and a nice throw can destroy a painting
15:46:41 <oklopol> oh the first guy is in the picture
15:46:49 <cpressey> I believe the point was "I can take panels from seperate Nancy strips and put them together into something that can be read, but does not make sense as we understand it"
15:46:54 <Phantom_Hoover> oklopol, have you considered that sometimes there is, in fact, no elaborately hidden punchline, and that the reason you cannot find one is not that you lack a sense of humour?
15:47:07 <Phantom_Hoover> This would perhaps be justified were you Vorpal, but you are not.
15:47:36 -!- MigoMipo has joined.
15:47:42 <cpressey> The objective of dada is to freeze the brain until the dressmakers' assistants arrive.
15:48:49 <Phantom_Hoover> cpressey, you should say to everyone "really, you don't get it? It's obvious!"
15:49:03 <oklopol> yeah no my approach didn't work
15:49:10 <Vorpal> Phantom_Hoover, not every comic strip has a punchline.
15:49:23 <Vorpal> depends a bit on which webcomic though
15:49:26 <cpressey> Phantom_Hoover: In my younger days...
15:50:01 <oklopol> has the author said there's no solution?
15:50:41 <cpressey> oklopol's use of the words "solve" and "solution" in regard to comic strips disturbs me somewhat.
15:50:51 <Phantom_Hoover> And Vorpal performs quite possibly the most amazing feat of oblivious demonstration the world has ever seen!
15:51:49 <oklopol> cpressey: if you directly see why a comic is funny, you didn't learn anything.
15:51:56 <Vorpal> Phantom_Hoover, of course, there are cases where either the author of the webcomic or the reader of it have different types of humour. That would give a similar end result.
15:52:27 <Phantom_Hoover> I don't think Vorpal even reads what other people say beyond the most cursory examination.
15:52:46 <Vorpal> Phantom_Hoover, I read the previous three lines + the highlight one
15:52:49 <cpressey> oklopol: that is true, although I am not always seeking to learn new things when I read a comic strip.
15:52:57 <Vorpal> (the previous ones to the highlight that is)
15:53:09 <Phantom_Hoover> This is particularly apparent whenever any form of subtlety is applied.
15:53:23 <Vorpal> Phantom_Hoover, but come on... comics like freefall doesn't use a punch line in *every* strip.
15:53:26 <cpressey> Vorpal, are you aware that we don't know what lines your IRC client highlights?
15:53:30 <oklopol> cpressey: well to be honest the only reason i read comics is to take a break from thinking.
15:53:40 <Vorpal> cpressey, "<Phantom_Hoover> This would perhaps be justified were you Vorpal, but you are not." had my nick in it
15:53:48 <Vorpal> pretty obvious it would highlight me
15:53:55 <Phantom_Hoover> Sarcasm being one thing he is utterly unable to detect or penetrate.
15:55:41 <cpressey> Anyway, xkcd pegged why R is the language of the future. It tells you that you're going to DIE
15:55:46 <oklopol> which year is this again? i have some trouble with time
15:56:24 <cpressey> oklopol: the sappy one with the statistics and the hugging, yes
15:56:39 <oklopol> well that's what i initially assumed, but the details don't quite seem to fit
15:56:50 <Phantom_Hoover> Ooh, Edinburgh apparently has in international science festival.
15:56:52 <Vorpal> oklopol, working out well. Not there today, the lab was cancelled. Lab was cancelled after the electricity system failed in that room. They were going to replace it today.
15:57:14 <oklopol> real life applications just told the reader it's about his disease
15:57:34 <Vorpal> oklopol, and how is it for you?
15:57:52 <cpressey> oh, oklopol didn't get the sappy part? ok, that was a misunderstanding on my part
15:57:53 <oklopol> Vorpal: trying to get my first publication this week
15:58:13 <oklopol> erm, i mean write my first article which i will then try to get published
15:58:16 <Vorpal> oklopol, ah. Good luck!
15:58:31 <cpressey> yes, the stick figure hates statistics because statistics are telling him that his friend/lover/co-stick-figure is gonna DIE
15:59:15 <Vorpal> hm, everyone will die sooner or later
15:59:20 <oklopol> yeah i get it now, i just didn't get what he meant by statistics having real life applications, but the applications were that they could predict shit and now that he's dying bleh
16:00:50 <Phantom_Hoover> There appears to be something about how the Vatican ascertains whether a miracle has occurred.
16:00:59 <Vorpal> oklopol, oh, it was a lab in a course about real time systems. Sadly this is "modern" compsci. Meaning it is more like computer programming/computer engineering often...
16:01:17 <oklopol> a chick bleeding out her vag ain't no miracle
16:02:05 <oklopol> i took this "theoretical" course on real-time systems and i can guarantee you that sucked more than yours ever could
16:02:24 <Phantom_Hoover> First she complained about the idea of firing nuclear waste into space because it would become our nuclear dumping ground.
16:02:40 <Phantom_Hoover> Y'know, because it's so easy to spoil the pristine landscape of space.
16:03:10 <oklopol> isn't the sun already slightly radioactive
16:03:16 <Vorpal> oklopol, well, we were going to program targeting vxworks. However, for some reasons booting more than a handful of the computers in that room made the fuse blow yesterday.
16:03:32 <Phantom_Hoover> Then, when someone mentioned that the universe was expanding, she said "if the universe is expanding what is it expanding into YOU CAN'T EXPLAIN THAT""
16:03:32 <oklopol> but i suppose it's nothing compared to whatever our nuclear plants produce
16:03:59 <Phantom_Hoover> So I was like "actually I can—" "NO YOU CAN'T YOU'RE JUST PRETENDING"
16:04:10 <cpressey> Phantom_Hoover: I think I'm in love
16:05:00 <Phantom_Hoover> Then I gave up because I previously had a long and bitter dispute with her over whether liquids could have pressure and you can't waste effort on stupidity of that magnitude.
16:05:09 <Vorpal> Phantom_Hoover, dumping nuclear waste in space would be rather expensive. Unless we build a space elevator (which would ALSO be expensive, though less so in the long run)...
16:05:43 <cpressey> whether... liquids can have... pressure... with a chemistry teacher
16:06:07 <cpressey> i mean, the other things, i can say, well, space, that's just not her domain
16:06:08 <Phantom_Hoover> Vorpal, well, the big problem with space dumping is that if the rocket explodes (not exactly a rare occurrence) you irradiate half of Europe rather than just the area around your train.
16:06:41 <Phantom_Hoover> cpressey, in fairness, she confused pressure with compressibilit— wait, I'm not giving her any quarter, that's just as bad.
16:06:45 <oklopol> well you can just slingshot the stuff into space
16:06:54 <Vorpal> Phantom_Hoover, that too. But even if that was solved, doing it by rockets would be far too expensive.
16:07:15 <oklopol> didn't the buld a rocket with a 20000 budget somewhere
16:07:34 <Vorpal> oklopol, 20000 of what?
16:07:46 <cpressey> some kind of solar-powered magnetic rail
16:08:37 <Phantom_Hoover> Vorpal, they're all, like, within 1.5 times each other.
16:08:42 <Vorpal> oklopol, I was referring to that 20000 SEK is a lot less than 20000 USD for example. :P
16:08:52 <oklopol> well right, but it's SMALLER
16:09:00 <Vorpal> Phantom_Hoover, I believe 1 USD is about 8 SEK or such
16:09:01 <oklopol> but i suppose you got that already
16:09:04 <Phantom_Hoover> Dammit where's pikhq I came up with the best Japanese joke.
16:09:05 <Vorpal> haven't checked in a while
16:09:14 <oklopol> i mean 20000 is ASTRONOMICALLY LESS than what rockets usually cost
16:09:25 <oklopol> who cares how many astronomers smaller it is
16:09:46 <Vorpal> oklopol, any idea about how much payload it could lift? And to what orbit?
16:10:07 <oklopol> oh i don't know, and i'm not even sure this story is true
16:10:30 <oklopol> that i doubt there's an intrinsic reason for rockets to cost a lot
16:10:50 <oklopol> rockets that just need to escape gravity
16:10:55 <cpressey> well, as I see it, it's the fuel that's expensive. thus: some kind of solar-powered magnetic railgun
16:11:08 <cpressey> It would probably have to be a few kilometers long, though
16:11:08 <Vorpal> one issue with rockets is that they need to haul the fuel they need to power themselves.
16:11:18 <Vorpal> which makes them heavier, needing more fuel
16:11:30 <cpressey> How long is the Forth Bridge again?
16:11:31 <oklopol> as for fuel, they're starting those daily flights to what was it 120km, and they use less fuel than a flight by jet from new york to X
16:11:40 -!- cheater- has joined.
16:11:44 <oklopol> again, completely unconfirmed random data
16:11:54 -!- cheater00 has quit (Ping timeout: 246 seconds).
16:12:09 <Phantom_Hoover> OH WAIT VORPAL IS HERE NO I DON'T KNOW ANYTHING ABOUT SCOTLAND I AM WELSH
16:12:41 <Vorpal> Phantom_Hoover, hrrm, I think I need to check logs on where you come from :P
16:12:57 <Phantom_Hoover> I AM TOTALLY NOT FROM THE CITY RIGHT NEXT TO THE FORTH BRIDGES
16:13:39 <Vorpal> that explains why I had no memory of you being from Wales when you claimed that recently. So indeed, you fooled me a for a while there.
16:14:12 -!- cheater00 has joined.
16:14:19 <Phantom_Hoover> (For the rail bridge; the road bridge is longer IIRC.)
16:15:50 <cpressey> I haven't worked it out -- such a railgun might have to be really, really long. Longer than the Forth bridge, was I guess what I was thinking, and how much does the Forth bridge cost to maintain annually? (rhetorical)
16:16:12 <cpressey> And it could only launch relatively light things
16:16:24 <cpressey> And I don't know that it could get them further than orbit
16:16:25 <Phantom_Hoover> "A billboard which featured a depressed goth and the slogan 'Cheer up Goth. Have an Irn Bru.' was also criticised for inciting bullying." — the ASA is basically the funniest thing ever.
16:16:27 -!- cheater- has quit (Ping timeout: 246 seconds).
16:16:35 <cpressey> But once in orbit, they could use rockets very very effectively
16:16:41 <Phantom_Hoover> (It's the UK body to which easily-offended people complain.)
16:16:58 <Vorpal> cpressey, I'm not sure you would get the same maintenance cost for a railgun and a bridge though.
16:17:07 <cpressey> Phantom_Hoover: yeah yeah har har har
16:17:41 <cpressey> Vorpal: no, but, same order of magnitude, i was guessing
16:17:54 <Vorpal> hm, I'm not qualified to answer that
16:18:00 -!- azaq23 has joined.
16:18:12 <cpressey> actually, you have to make damn sure the rail is nice and ... rail-y, you really wouldn't want your nuclear waste derailing at the end
16:18:46 <cpressey> although, better the Gobi desert (or whereever) than all of Europe, as I think PH mentioned
16:18:55 <Vorpal> quite. Hm how would it work? Would it be straight or would it curve upward at the end?
16:19:19 <cpressey> If it was straight, it would have to be REALLY long
16:19:43 <Vorpal> cpressey, if it had to go at an angle upwards I suspect it would need rather more complex supports (unless you found a suitable mountain side to use), which would probably drive up the price.
16:19:47 <cpressey> If it curves upward... that seems like it would be harder to do
16:20:19 <cpressey> And computing the speed necessary for the mass and the angle, to get it into orbit, and not have it fall back... well, we have computers.
16:20:40 <Vorpal> yeah I don't think that is the largest issue
16:21:08 <cpressey> and once it's outside the atmosphere, that's when you start the rockets. they don't need much fuel because you're outside of the drag and much of the gravity.
16:21:43 <cpressey> yeah, so let's build this sucker
16:21:48 <Vorpal> when I said rockets were expensive, I meant from the surface of the earth.
16:22:32 <cpressey> I think the name 'Irn Bru' is inherently bullying.
16:23:06 <Vorpal> cpressey, hm does it need to get into an east/west-wards orbit or could you launch it straight south? In the latter case you could build it pointing along the Atlantic. Very few inhabited islands there. Very few islands even.
16:23:31 <Vorpal> would be good in case of accidents.
16:23:54 <Vorpal> less risk of damage in case it doesn't reach orbit
16:24:23 <cpressey> I don't know. I don't see why not
16:26:08 <Vorpal> I seem to remember there is some complication with getting into polar orbits. Hm...
16:27:55 <cpressey> Possibly, but the wp article doesn't suggest anything really difficult
16:28:48 <Phantom_Hoover> Also you have to correct for the earth's rotation as well.
16:29:52 <Phantom_Hoover> Actually I think the second point is the main one, particularly as rockets tend to be launched from fairly low latitudes.
16:30:29 <cpressey> well, if the destination is orbit, the railgun approach gives you very limited options, no matter which way it's pointing
16:33:42 <cpressey> I like the wheels idea. Especially putting a block behind every wheel so the thing doesn't move (much) when you fire it. Like on artillery.
16:34:57 <cpressey> Uh, whatever's most conventient, if the ultimate purpose is to get spent nuclear fuel into the sun or whatever
16:35:35 <Vorpal> Phantom_Hoover, not sure. I was thinking polar one because if you place it in, say, UK, then you can fire pretty much across the Atlantic. Which is very sparsely inhabited. Which is a bonus in case of accidents
16:36:09 <Vorpal> well, actually I guess along the Antarctic
16:36:44 <oklopol> what's the fuel consumption difference between to orbit vs shot into space?
16:36:44 <Vorpal> Phantom_Hoover, isn't that the wrong direction too? With regards to Earth's spin...
16:37:03 <oklopol> or is it relative depending on what shooting means
16:37:29 <oklopol> i would've thought once you get to orbit, it's relatively easy to get out completely, but actually i suppose the orbits are rather closed compared to earth's radius
16:38:00 <cpressey> a really elliptical orbit might be good then -- you could get out of it at the far point
16:38:22 <oklopol> oh we were still talking about completely escaping
16:38:31 <Vorpal> cpressey, once you get far enough I suggest ITN for low energy transfer towards the sun.
16:38:40 <oklopol> i don't see why just leaving that shit on the orbit would be all that dangerous
16:39:05 <Vorpal> (http://en.wikipedia.org/wiki/Interplanetary_Transport_Network)
16:39:38 <Vorpal> Phantom_Hoover, so would it be better to go to orbit and then break away rather than break away directly?
16:39:50 <oklopol> Phantom_Hoover: so does your mom but i still keep doing her
16:40:08 <Phantom_Hoover> Yes, because thrusting from orbit doesn't have the complications that it does on a planet.
16:40:21 <oklopol> i'll be dead by the time they come down so what do i care
16:40:24 <Vorpal> Phantom_Hoover, right.
16:40:24 <Phantom_Hoover> (I know what oko is going to say, so he needn't bother.)
16:41:09 <oklopol> Phantom_Hoover: erm what, thrusting your mom from orbit doesn't have the complications the it does on a planet?
16:41:49 <oklopol> maybe in orbit, now it doesn't quite look like the correct kind of thrusting
16:42:40 <oklopol> the point of the mom joke was just to attract attention to the classical philosophical problem of i don't give a shit what happens after i die
16:43:04 <oklopol> now that it's obscure not-really-a-joke explanation day
16:44:54 <oklopol> but having sex weightless is one of the fundamental experiences in life
17:10:25 -!- R-Type has quit (Remote host closed the connection).
17:11:08 <cpressey> <cpressey> Vorpal: Well: I wanted to write a bot in R, just because R is a horrible language to do such a thing in. I named it 'R-Type' because 'rbot' was taken, 'R-bot' is boring, and R-Type was a significant game in the history of video games (not a huge favorite of mine, but I can appreciate it.) Since the point was just to write a bot in R, I didn't care what it actually did. So...
17:11:15 <cpressey> So I modelled its personality after a cat I met once.
17:11:46 <oklopol> R-Type is a computer robot
17:12:11 <oklopol> R-Type is a computer robot
17:12:19 -!- cheater- has joined.
17:14:54 -!- cheater00 has quit (Ping timeout: 246 seconds).
17:15:46 <cpressey> Phantom_Hoover: I don't think so. That's the 3D wireframe one for the 8-bits, isn't it?
17:17:42 <Ilari> APNIC down 0.03: 64k+/32 to Australia, 64k to China, 256 to Hong Kong, 1024+256 to Indonesia, 1k+256+/32 to India, 64k+8k+1k to Japan, 2k to South Korea, 1k to Nepal, 256 to Philipphines, 256+/32 to Singapore, 4k to Thailand, 256k+64k+8k to Taiwan.
17:19:07 <Ilari> Depletion estimate: Thursday 14th April.
17:29:41 -!- cheater00 has joined.
17:30:39 -!- cheater- has quit (Ping timeout: 246 seconds).
17:34:06 -!- iamcal has joined.
17:41:44 <Vorpal> Ilari, any idea how accurate that estimate is?
17:43:09 <Ilari> No idea. These processes are highly discrete and distributions behave badly. Fourth quadrant stuff for sure.
17:45:36 <Ilari> Basically, the APNIC pool is so depleted that one huge allocation could take most of it and then the rest of the allocations on that day would finish it off.
17:47:50 <Ilari> It could be tomorrow, we might make next week without depletion, nobody outside APNIC really knows.
18:09:26 -!- ben_ has joined.
18:11:00 -!- oerjan has joined.
18:22:09 -!- ben_ has left ("Ex-Chat").
18:23:56 <oerjan> <cpressey> Longhair + living on the streets = permanent knots in fur = quite painful, I imagine = not the happiest individual.
18:24:16 <oerjan> um can't they cut it off...
18:27:56 <oerjan> <oklopol> like, that many survive 5/10 years of X
18:28:03 <oerjan> that was my guess when i read it...
18:28:35 <oerjan> randall munroe _has_ some disease in the family
18:29:29 <cpressey> oerjan: i believe they were trying to do that, at the time (this was years ago), but something about the knots being close to the skin made it difficult to shave
18:29:46 -!- asiekierka has quit (Ping timeout: 240 seconds).
18:30:26 <cpressey> The cat whose personality R-Type's is modelled after.
18:30:45 <oerjan> vietnamese rolling furball
18:33:12 <oerjan> <cpressey> I mean, I have seen xkcd's involuntarily on peoples' shirts and hanging in their cubes, and it didn't damage me *too* much.
18:33:24 <oerjan> those _would_ tend to be the less damaging ones, one would think
18:33:59 <oerjan> except maybe someone probably has one of the worst ones just for the hell of it...
18:34:27 <oklopol> he would have to constantly explain it
18:34:58 <oerjan> well i mean like that infamous genitals one...
18:35:11 <oklopol> i don't think a comic can be stupid enough that... erm which one is that?
18:36:27 <Phantom_Hoover> Don't think too hard about the joke in that one either.
18:38:08 * oklopol tries not to think about it
18:38:42 -!- elliott has joined.
18:39:08 <oerjan> <oklopol> fun little problem: find a 5-regular planar graph, where 5-regular = every vertex has degree 5
18:39:50 <elliott> 06:58:51: <oerjan> <elliott> (I am pretty sure Eliezer Yudkowsky once said "a".)
18:39:51 <elliott> 06:59:27: <oerjan> it would be rather impressive if somehow he has carefully avoided a particular common word for years without being detected.
18:40:02 <elliott> maybe "Eliezer Yudkowsky" is an anagram...
18:40:19 <oklopol> oerjan: that was mister x's solution, he said he tried x-hedron and it didn't work so he tried z-hedron and it did
18:40:57 <oklopol> but you don't know what an icosahedron is (i sure as hell don't) to be able to come up with that
18:41:00 <oklopol> if you think about a 3d ball
18:41:15 <oklopol> to come up with *a* solution
18:41:29 <oerjan> you mean there's anything simpler than an icosahedron?
18:41:33 <elliott> 14:57:31: <tswett> elliott: but really, is PerlNomic better than another nomic we could come up with?
18:41:54 <elliott> tswett: Is skiing better than Chess?
18:41:59 <oklopol> i have two constructions that give 12 + 4k vertices
18:42:01 <oerjan> 12 vertices (it's dual to dodecahedron)
18:42:23 <oerjan> then your k=0 may be that
18:42:37 <oklopol> one of them gives some hedron as the 12 case, i don't know about the other one
18:42:52 <oklopol> cpressey: interestingly enough, no!
18:43:39 <oklopol> where - is set theoretic subtraction since you're smartasses
18:45:15 <cpressey> tuples of small categories, that is
18:45:39 <oklopol> oerjan: take two vertices, one to the left, one to the right of the ball, and for any k put 5(k + 2) C_5's around the ball somewhere between the two side vertices, then connect the side vertices to the points of the C_5 next to them, and for adjacent C_5's, connect each point to two points of the next C_5
18:45:53 <oklopol> kind of hard to explain but maybe you'll get it
18:46:17 -!- elliott has quit (Remote host closed the connection).
18:46:34 <oklopol> that's equivalent to an icosahedron when k = 0
18:48:34 <oklopol> in this case i'm putting them on a sphere so pentagon is not really a good term
18:50:08 <cpressey> <oklopol> fun little problem: find a 5-regular planar graph, where 5-regular = every vertex has degree 5 <--- wait what?
18:50:25 <oklopol> hey so last night or last week or whatever i proved that tally sets can't be NP-complete, didn't i do some stuff on left sets here at some point?
18:50:27 <cpressey> do the edges have to be straight or something?
18:50:32 <oklopol> maybe if i don't remember, no one will
18:50:33 <oerjan> ...but the faces of a dodecahedron are pentagons
18:50:57 -!- elliott has joined.
18:51:08 <oklopol> oerjan: if you put a C_5 around a sphere, there are no angles
18:51:20 <cpressey> because if not, just have two vertices, and 5 edges between them. done. planar as all hell
18:51:35 <elliott> oklopol: OR ARE THERE INFINITE ANGELS
18:51:47 <oklopol> cpressey: using the usual definition of graph here
18:51:51 <oklopol> just one edge and no self-loops
18:52:22 <oklopol> oerjan: or did you mean there can't be an isomorphism between the result of the construction and an somethinghedron?
18:52:27 <oklopol> cpressey: between each pair
18:52:44 <cpressey> no multigraphs or whatever they call that
18:52:51 <oklopol> they often call them multigraphs
18:53:03 <oerjan> oklopol: i'm just pointing out pentagons can be used for this, in a sense...
18:53:07 <oklopol> but definitions differ a lot in gt
18:53:23 <oerjan> although that's mixing faces and vertices with the duality
18:53:57 <oklopol> you can use all kinds of things if you're smart enough
18:54:29 <oerjan> I USE A PROJECTED PENROSE TILING FROM HYPERSPACE
18:56:02 <oklopol> a more fun problem: show that a 4-critical graph is either a wheel of even order or it contains no wheels as a subgraph
18:56:12 <oklopol> no theorems needed, but a lot of definitions
18:56:53 <oklopol> 4-critical = exists proper 4-coloring of vertices, and no 3-coloring, but in any proper subgraph there exists a 3-coloring
18:57:30 <oklopol> wheel of order n = C_{n-1} + a node connected to each of its points
18:58:16 <cpressey> i'd rather do the what you call "kids math"
18:58:22 <oklopol> the solution presented in our homework session was wrong, followed by the official solution by the professor, which was also wrong :D
18:58:27 <oklopol> (although only slightly wrong)
19:03:33 <oerjan> <oklopol> isn't the sun already slightly radioactive
19:04:21 <oerjan> if by radioactive you mean "occasionally sends out enough charged particles to kill an unprotected human"
19:05:03 <oerjan> no, earth is protected by its magnetic field and atmosphere
19:05:31 <oklopol> well i don't know any of that fancy magnet stuff but i like the idea of being protected.
19:06:08 <oerjan> in fact the atmosphere is supposedly itself protected by the magnetic field, without it the radiation would slowly whittle the atmosphere away
19:06:14 <cpressey> I almost did it with 8 vertices, but I have one edge that goes between two vertices that already have an edge.
19:06:32 <oerjan> which may have happened on mars
19:06:52 <elliott> 22:02:54: <cpressey> strsplit(gsub('^:(.*?)\\!(.*?)\\s+PRIVMSG\\s+(.*?)\\s+\\:(.*?)$', '\\1\u2603\\2\u2603\\3\u2603\\4', line, perl=TRUE), '\u2603', fixed=TRUE)
19:07:07 <cpressey> so, um, 16 vertices, which is in fact 12 + 4k when k=1! cool
19:07:21 <oklopol> can you describe it somehow?
19:07:40 <cpressey> oklopol: make a copy of it, then hook up the two copies with two edges where I had the extra edge in the one
19:07:51 <elliott> 22:28:22: <cpressey> (I've modelled its personality after a cat I met once)
19:07:51 <elliott> did its eye pop out and did you eat it and absorb its esoteric powers
19:08:33 <oklopol> cpressey: i don't think you can do that planarly but maybe i'm mistaken
19:09:02 <cpressey> oklopol: it's possible i miscounted the # of edges here. maybe i'll try to draw it more neatly
19:09:14 <oklopol> actually it's possible planarly, if i know what you mean
19:09:15 <elliott> 23:08:42: <Vorpal> but really. R, J, K are all array processing languages. And have one letter names. There might be a pattern there. Should be investigated further.
19:09:20 <elliott> i don't think Vorpal quite knows what R is
19:09:45 <elliott> 23:11:12: <cpressey> K is rather insane. Maybe... naw.
19:09:49 <elliott> cpressey: it's probably been done :>
19:10:12 <elliott> 23:58:26: <tswett> It annoys me that there are global constants (variables?) that aren't classes.
19:10:12 <elliott> 23:58:32: <tswett> Transcript and Smalltalk, for example. Maybe others.
19:10:18 <cpressey> elliott: I couldn't find an implementation of K anyway. In the 4 whole seconds I spent looking
19:10:37 <elliott> cpressey: Pay up, or get K3 (the cool one with the GUI thing) from a hidden subdirectory of nsl.com :)
19:10:40 <oklopol> as they say, 5th second is the charm
19:10:51 <oerjan> <Vorpal> that explains why I had no memory of you being from Wales when you claimed that recently. So indeed, you fooled me a for a while there.
19:11:02 <oerjan> bah, no one outside britain knows the difference anyhow
19:12:15 <oerjan> just strangely unpronouncible places with bagpipes and leprechauns and whiskhey
19:12:53 <oerjan> and green. lots of green.
19:14:00 <elliott> 03:31:56: <augur> oklopol: well, you can do math in agda!
19:14:11 <elliott> this is to embarrassing to read
19:14:17 <elliott> oklopol: i swear us dependent type guys aren't that bad
19:14:35 <cpressey> whoops. oklopol: i actually have 2 multiedges. dammit
19:14:49 <oklopol> cpressey: took me 45 minutes to come up with a solution
19:15:02 <elliott> 03:35:30: <oklopol> i imagine doing math in agda would be similar to programming in brainfuck, sure it can be fun but you'll be proving 1+1=2.
19:15:17 <elliott> oklopol: does gödel's incompleteness theorem count as 1+1=2? :D
19:15:19 <elliott> well, that was actually coq.
19:15:25 <oklopol> well maybe not quite that long but longer than oerjan's 5 seconds
19:15:50 <elliott> oklopol: no, russell o'connor did: http://r6.ca/Goedel/goedel1.html
19:16:08 <oklopol> and was he an amateur at coq?
19:16:15 <oklopol> gdel's theorem isn't all that deep
19:16:23 -!- wareya has quit (Read error: Connection reset by peer).
19:16:26 <elliott> "Because my proof is constructive, it is possible, in principle, to compute this sentence that makes PA incomplete." ;; this is the coolest part :)
19:16:42 <cpressey> > let true & false = true in true & false
19:16:42 <oerjan> <Phantom_Hoover> (It's the UK body to which easily-offended people complain.)
19:16:43 <lambdabot> Not in scope: `true'Not in scope: `false'
19:16:57 <oerjan> what we need is mandatory sterilization of easily offended people.
19:17:30 <oklopol> we computed many sentences that make PA incomplete in automata theory
19:17:37 -!- wareya has joined.
19:17:45 <elliott> 08:57:33: <mtve> quite esoteric - http://arxiv.org/abs/1104.0924v1
19:18:05 <oklopol> it's not rocket science, and in any case i'm talking about what an amateur can do
19:18:06 <elliott> oklopol: well this is the gödel one :P
19:18:20 <elliott> oklopol: printing it before we all die is impossible though. and that is because it is a poison.
19:20:28 <cpressey> > let True & False = True in True & False
19:20:46 <elliott> 12:32:10: <Ilari> Hah. I seemingly got signed up to one mailing list in "opt-out" fashion (quite understandable given the situation).
19:20:47 <elliott> 12:33:27: <Ilari> Well, basically one mailing list was shut down and new one created to continue (apparently mailman can't rename mailing lists).
19:20:53 <elliott> Ilari: this wouldn't happen to be the ffmpeg/libav fiasco?
19:21:12 <cpressey> it wasn't a fiasco, it was an imbroglio
19:22:12 <oerjan> <cpressey> I haven't worked it out -- such a railgun might have to be really, really long. [...] <-- i have this hunch part of the problem is you don't want the speed to get too high until you've passed most of the atmosphere...
19:22:13 <elliott> Ilari: with /that/, the people who had, two months prior, attempted to perform a ridiculous coup d'etat on the project forked off and made a new mailing list, then subscribed every member of the ffmpeg mailing list to their new one, claiming it was just a "project rename"
19:22:28 <elliott> Ilari: (they then used their technical control of the ffmpeg lists to shut them down, telling everyone to move to the "newly-renamed" libav lists)
19:24:06 <elliott> Phantom_Hoover: because they didn't like how the maintainer was handling proposed patches
19:24:43 <elliott> a perfectly valid complaint, but trying to take over the project without telling anyone through technical means without trying to discuss it or even fork is enough to make me not give a damn what they're complaining about
19:24:58 <elliott> Phantom_Hoover: I think he was rejecting patches based on what they saw as trivial grounds or something
19:27:48 <cpressey> I have a code review that is three pages long (ReviewBoard pages -- I'm not sure how it decides how long a page is) that is boring me out of my skull
19:28:21 <cpressey> You know, when you almost entirely rewrite something, diffs are almost entirely useless
19:30:43 * elliott watches cpressey slowly give up on life
19:36:42 <cpressey> I am becoming more and more convinced that programming (heavily, exclusively) in Python changes the way you think for the worse.
19:38:57 <elliott> cpressey: only suicide can cure you
19:39:04 <elliott> Do not attempt suicide because of this line.
19:39:11 <elliott> (Attempt it because of the line three lines up instead!)
19:39:38 -!- Sgeo has joined.
19:39:39 <elliott> 16:16:25: <Phantom_Hoover> "A billboard which featured a depressed goth and the slogan 'Cheer up Goth. Have an Irn Bru.' was also criticised for inciting bullying." — the ASA is basically the funniest thing ever.
19:39:46 <elliott> Phantom_Hoover: well people might whack goths with irn brus
19:40:04 <elliott> dammit, i should stop giving ph ideas
19:40:21 <cpressey> idea: language where all expressions have side effects. an integer expression is in fact of the form kB where B is a block of code (possibly empty) that is executed k times.
19:40:26 <elliott> is it just me, or is wikipedia's new anti-vandal policy is to show the edit button as "View source" until you click it, if you're not logged in?
19:40:39 <elliott> it's ingenious in its stupidity
19:48:20 <elliott> cpressey really likes this part of haskell
19:50:36 <cpressey> > let in let in let in let in let in let in "let"
19:50:44 <oerjan> > let a = 5 where in a
19:50:56 * Sgeo is reading about the Maude language
19:51:09 -!- azaq23 has quit (Quit: Leaving.).
19:51:10 <lambdabot> <no location info>: parse error on input `in'
19:51:21 <cpressey> Sgeo: I never got very far with Maude
19:51:30 <cpressey> I... just tried to tab-complete Maude, though
19:53:07 <oerjan> > let a | otherwise = b where in a
19:54:01 <lambdabot> <no location info>: parse error (possibly incorrect indentation)
19:54:15 <elliott> cpressey: watchoo do to http://catseye.tc/lab/robin/robin.html, i'm logreading and broken links totally destroy my flow
19:54:17 <elliott> oerjan: omg that would be awesome
19:54:26 <lambdabot> <no location info>: parse error on input `;'
19:54:32 <elliott> let in do let; let in do let; let; "hi"; let in do let
19:54:51 <oerjan> > let in do let in do let in do let in "hi"
19:55:02 <elliott> 16:22:32: <cpressey> I think the name 'Irn Bru' is inherently bullying.
19:55:10 <elliott> cpressey: really? well i guess it's kinda cheesy
19:55:13 <elliott> I GUESS YOU JUST HAVE TO GROW UP WITH IT
19:55:36 <cpressey> it suggests the lowest-class pronunciation in my head
19:55:50 <cpressey> don't know if that was intentional or what
19:55:53 <elliott> cpressey: it's probably meant to
19:56:02 <elliott> i don't really parse it out as, you know, iron brew
19:56:45 <elliott> Irn-Bru and Diet Irn-Bru have been formulated since 2002 by A.G. Barr plc to meet the regulations for food colouring of the U.S. Food and Drug Administration. Ponceau 4R used in the UK formulation is prohibited by U.S. Food and Drug Administration (FDA). Barr's uses alternative food and drink colourants manufactured by a US Company approved by the FDA. The product labelling also meets US labelling standards on nutritional information and bar code
19:56:46 <elliott> . Compliant Irn-Bru is solely imported by Great Scot International in Charlotte, North Carolina, who supplies distributors and retailers throughout the US. It is only supplied in 16.9 fl.oz.
19:56:53 <elliott> cpressey: HA, YOUR PUNY COUNTRY CAN'T HANDLE SCOTTISH METAL DRINK
19:57:13 <elliott> 16:30:59: <Phantom_Hoover> UNLESS you put it on a GIANT TURNTABLE
19:57:20 <oerjan> wait you mean irn bru isn't something fancy gaelic?
19:57:48 -!- ais523 has joined.
19:58:36 <oerjan> they made irn bru technically illegal with no penalty just so ais523 couldn't drink it
19:59:07 <ais523> I wouldn't drink it anyway, I don't like that sort of thing
19:59:44 <Sgeo> There's something... fun about Maude's infix operators
20:00:27 -!- Slereah has quit (Ping timeout: 276 seconds).
20:01:03 <oerjan> we need a language with non-euclidean operators
20:01:26 <Phantom_Hoover> As the channel's resident expert on stupid non-Euclidean things, I approve.
20:01:27 <oerjan> the kind Man was Not Meant to Know
20:01:59 <elliott> Phantom_Hoover: i'm gonna BLOW YOUR MIND
20:02:01 <elliott> Phantom_Hoover: the universe
20:02:06 <elliott> Phantom_Hoover: is NON-EUCLIDEAN
20:02:08 <Zwaarddijk> so this language should be C(noneuclidean operator)^2
20:04:27 <augur> elliott: fuck you :|
20:04:54 <augur> agdas pretty neat tho
20:05:26 <elliott> why waste all your time proving things that would take three seconds in coq :)
20:05:48 <elliott> augur: proving things in agda is a bitch. compared to coq
20:06:33 <augur> elliott: maybe. its not /too/ bad, i find. i like how it forces you to understand the structure of the proof, which i feel is good if im going to be writing papers using a proof assistant as a tool
20:06:44 <augur> i dont want to have to explain the magic of coq on top of stuff
20:06:44 <elliott> ITT: augur has never used coq ever
20:07:04 -!- Slereah has joined.
20:07:07 <elliott> proofs in agda == proofs in coq. coq just has tools to help you write them, and agda doesn't.
20:07:24 <augur> what tools does coq have?
20:07:30 <elliott> proofgeneral's interface to the toplevel.
20:07:38 <augur> ill have to take a look
20:07:42 <elliott> you can see all your assumptions and your current goal, plus the goals left after that
20:07:48 <elliott> and undo proof steps, etc.
20:08:03 <augur> i dont mind the agda stuff. its fun to figure out how to construct it.
20:08:08 <augur> but ill take a look at coq
20:08:11 <elliott> although if he's avoiding "magic" (like agda's library isn't magic?) he might want to avoid "auto" :)
20:08:19 <elliott> augur: turn on three window mode and electric terminator in proofgeneral
20:08:21 <augur> im not using much of agda
20:08:53 <elliott> because you're using its proof combinators
20:08:58 <elliott> unless you're writing proofs in direct functional style
20:09:07 <elliott> (setq proof-three-window-enable t)
20:09:15 <elliott> and (setq proof-electric-terminator-enable t)
20:09:20 <augur> what do you mean in direct functional stuff
20:09:28 <elliott> augur: paste a proof/lemma
20:09:33 <elliott> i'll tell you whether you're using the library or not
20:09:43 <elliott> (protip: if there's unicode, you are)
20:09:59 <augur> i use unicode a lot.
20:10:20 <elliott> augur: i mean apart from the things you type.
20:10:31 <elliott> if there are unicode things in your source file that aren't names you made up
20:10:59 <elliott> then that's magic. if you don't believe me, look at its source sometime.
20:11:23 <augur> http://hpaste.org/45440/syntax_crap
20:11:33 <augur> look at whats source
20:12:08 <elliott> the stdlib's. why are you making this simple conversation so painful X_X
20:12:40 <elliott> oh nice, you're actually copy-pasting the stdlib directly in.
20:12:51 <augur> not copy and pasting anything
20:12:59 <elliott> welp, typical unicode agda noise :)
20:13:00 <augur> are you referring to danielsson's standard library?
20:14:00 <augur> part of the reason im doing it this way is that i want to understand the structure of the program as completely as possible, and making it myself helps me understand
20:14:09 <elliott> i am referring to the agda standard library
20:14:16 <elliott> http://www.cse.chalmers.se/~nad/listings/lib-0.5/README.html
20:14:57 <augur> and part of it is that if i have to explain some crap to anyone who asks (who isnt so good on all of this mathylogicy stuff) i'd like to be able to give them a clean answer from the source code directly
20:15:08 <augur> without referencing some magic library off somewhere in the ether
20:15:18 <elliott> or, you know, just linking to its source
20:15:29 <augur> except thats more problematic if im giving a presentation.
20:15:37 <augur> and someone asks about this or that
20:15:41 <elliott> anyway, i can't see any of this being very easy to explain because like most agda it uses unicode tricks and mixfix to obscure the point
20:15:50 <augur> then i have to try and remember what the standard lib says etc etc whatever
20:15:53 <elliott> i see they still noise up their code with explicit level wrangling, too
20:16:29 <augur> i rather like the unicode and mixfix
20:16:31 <augur> why dont you like it?
20:16:55 -!- azaq23 has joined.
20:24:06 -!- Slereah has quit (Ping timeout: 246 seconds).
20:24:38 -!- azaq23 has quit (Quit: Leaving.).
20:26:10 <augur> coq looks interesting
20:26:57 -!- azaq23 has joined.
20:27:02 <augur> i dont follow the structure of the proofs tho
20:27:04 -!- cheater99 has joined.
20:28:06 -!- cheater00 has quit (Ping timeout: 246 seconds).
20:28:59 <augur> i understand agda proofs -- if it type checks, youve got a proof
20:29:05 <augur> i dont get coq at all
20:29:31 -!- Slereah has joined.
20:34:17 -!- Sgeo has quit (Ping timeout: 258 seconds).
20:36:37 <Gregor> Hmmm, OmniGraffle is the only graphical tool I've ever used that I would say is appropriate for people with OCD :P ... mmm, maybe also Minecraft.
20:41:09 <elliott> <augur> i understand agda proofs -- if it type checks, youve got a proof
20:41:13 <elliott> augur: uhh, same with Coq?
20:41:37 <ais523> apparently someone rewrote xmonad in Coq
20:41:39 <ais523> just because they could
20:41:46 <elliott> ais523: stop being slashdot
20:41:53 <ais523> (with the normal Reddit-related meaning of "apparently")
20:41:59 <elliott> not even reddit had that, I've seen the posts
20:42:12 <elliott> "We rewrote parts of xmonad's core algorithms in Coq to prove them correct and extracted the results to Haskell"
20:42:23 <elliott> "Someone rewrote xmonad in Coq!"
20:42:37 <tswett> elliott: no, Transcript and Smalltalk are not classes.
20:42:44 <elliott> tswett: well, they're objects
20:42:47 <augur> elliott: perhaps! but the proofs also have all these other things
20:42:54 <ais523> beh, it'd have been more fun if there was no reason
20:42:56 <augur> unfold f, g. destruct h. etc etc
20:42:59 <elliott> augur: yes, those are tactics
20:43:04 <elliott> augur: if you "Print proof_name"
20:43:10 <tswett> elliott: I define "better" as "skiing is not better than chess, nor vice versa".
20:43:13 <elliott> the tactics just make proofs about 159% easier to write
20:43:33 <elliott> tswett: Then I say that your question is unanswerable.
20:43:52 <elliott> Perhaps any new came-up-with game would be better technically, or in some other sense, than PerlNomic, but that does not mean it would be a better game.
20:43:58 <elliott> I'd say that both are games worth playing.
20:45:57 <tswett> Say, elliott, would you happen to know of an implementation of a Lisp that has Smalltalk-esque orthogonal persistence? :P
20:46:25 <elliott> Well, just about every Common Lisp implementation lets you save the current world.
20:46:44 <tswett> That sounds desirable.
20:47:43 <olsner> flrgbl flrbgl shfpngr!
20:47:55 <elliott> tswett: Yes, but, Common Lisp.
20:47:58 <cpressey> Someone rewrite skiing's core algorithms in chess to prove them better and extracted the results to xmonad.
20:48:08 <elliott> I like the change of tense there
20:48:17 -!- Sgeo_ has joined.
20:48:44 <tswett> I think all mathematics should be developed with the goal of using it in a window manager.
20:49:00 <tswett> Mathematical research should follow this algorithm:
20:49:13 <elliott> omg, does this mean that the singularity will manage windows for me
20:49:22 <elliott> and figuring out my desired arrangement
20:49:47 <tswett> 1. Think of an idea. 2. Make hypotheses about the idea. 3. Prove as many of the hypotheses as possible. 4. Incorporate all resulting theorems into xmonad.
20:50:43 -!- BeholdMyGlory has quit (Remote host closed the connection).
20:56:38 <cpressey> This message has been translated into French.
20:57:42 -!- impomatic has quit (Quit: ChatZilla 0.9.86.1 [Firefox 3.5.18/20110319140258]).
20:58:20 <augur> cpressey: ce message a trad.. a francais
20:58:21 <Phantom_Hoover> <elliott> Well, just about every Common Lisp implementation lets you save the current world. ← I don't recall non-SBCL or CMUCL having it, but I wasn't exactly thorough.
21:07:44 <cpressey> I hope to never, ever program anything in that language.
21:08:51 -!- Sgeo_ has quit (Ping timeout: 260 seconds).
21:10:47 <elliott> cpressey: Err, what, Lisp?
21:13:28 <elliott> cpressey: Better experience than 99% of languages...
21:16:49 <cpressey> Well, Common Lisp specifically.
21:17:09 <elliott> cpressey: I stand by my statement :)
21:17:50 <elliott> cpressey: Admittedly the modern /environments/ aren't so ideal.
21:18:09 <elliott> But the language itself is something I'd much rather have to code in than almost every other language.
21:18:14 <elliott> (There are maybe ten exceptions.)
21:18:38 <Phantom_Hoover> Epigram 2 doesn't count due to not existing in any meaningful way.
21:21:42 <olsner> too few languages to warrant making a list
21:22:10 <olsner> anyway, EVERYTHING SUCKS
21:22:30 <elliott> olsner: you're either mocking me perfectly, or are a man I can relate to.
21:22:37 <oerjan> it's a Maybe (Exception, Maybe (Exception, Maybe (Exception, Maybe (Exception, Maybe (Exception, Maybe (Exception, Maybe (Exception, Maybe (Exception, Maybe (Exception, Void)))))))))
21:22:38 <cpressey> As long as Scheme is one of the exceptions, it kind of wins out, for me.
21:23:18 <elliott> cpressey: Yeah, but if you were groaning at the lack of standardised names... at least the name for common list operations are the same in every Common Lisp :P
21:23:33 <elliott> cpressey: And, sure, but, Common Lisp or PHP?
21:23:39 <elliott> Common Lisp or Python? Perl? C? Ada?
21:23:55 <elliott> cpressey: I... am floored that you know what Pharen is.
21:24:17 <cpressey> I heard [about it] through the grapevine
21:24:23 <olsner> "a compiler that takes a Lisp-like language and turns it into PHP" :/
21:24:32 <elliott> cpressey: was just about to correct you BRO
21:25:04 <elliott> I mean, 90% of languages are really bad.
21:25:16 <elliott> 9% of the rest are tolerable but not any good.
21:25:27 <elliott> I'd say Common Lisp almost certainly belongs to the remaining 1%.
21:25:34 <cpressey> I would totally program in C for fun before I would program in Common Lisp for fun.
21:25:58 <elliott> cpressey: I don't really see how you could place Scheme above 'em but CL below C.
21:26:12 <elliott> Sure, the multiple namespaces is a bit crappy, and a lot of the standard names suck but... it's still Lisp
21:26:48 <elliott> Well, right, CLOS is one of the two tolerable OOP systems out there :)
21:29:03 <cpressey> elliott: I qualified my statement with "for fun" -- I am not concocting an absolute total order here.
21:29:48 <cpressey> I mean, dude. I just wrote a bot in R.
21:29:48 <elliott> Confound your imprecision!
21:29:59 -!- MigoMipo has quit (Read error: Connection reset by peer).
21:30:04 <cpressey> Do I put R above Common Lisp? Apparently!
21:32:07 <cpressey> right now I have to debug Javascript :( not by choice obv
21:34:03 <olsner> Y U PUT BUG IN PROGRAM? well, now you get to take it out...
21:34:11 <elliott> cpressey: "Ten days without much sleep to build JS from scratch, "make it look like Java" (I made it look like C), and smuggle in its saving graces: first class functions (closures came later but were part of the plan), Self-ish prototypes (one per instance, not many as in Self)."
21:34:20 <elliott> cpressey: ONLY KINSHIP WITH BRENDAN EICH CAN SAVE YOU
21:34:44 <Phantom_Hoover> cpressey, have I mentioned the time my school told everyone to use IE 5 *for Mac* to run JS.
21:35:07 <cpressey> Phantom_Hoover: yes. olsner: Django. (no further words are needed)
21:35:30 <elliott> Phantom_Hoover: Actually IE 5 for Mac was an okay browser.
21:35:33 <elliott> It shared no code with the Windows version.
21:35:56 <elliott> cpressey: listen to Django Reinhardt while doing it, it'll be SO IRONIC (hipster for "worthwhile, validating experience")
21:36:18 <elliott> cpressey: (I have never listened to Django Reinhardt and don't plan to)
21:36:20 -!- cheater00 has joined.
21:38:06 -!- cheater99 has quit (Ping timeout: 246 seconds).
21:38:13 <olsner> django is named after a person?
21:38:23 <olsner> thought it would be a giraffe or something
21:40:43 <elliott> `addquote <olsner> django is named after a person? <olsner> thought it would be a giraffe or something
21:40:46 <HackEgo> 353) <olsner> django is named after a person? <olsner> thought it would be a giraffe or something
21:42:25 -!- Phantom_Hoover has quit (Remote host closed the connection).
21:43:37 -!- olsner has quit (Ping timeout: 276 seconds).
21:44:52 <elliott> "In Tron, the hacker was not supposed to be snooping around on a network; he was supposed to kill a process. So we went with posix kill and also had him pipe ps into grep. I also ended up using emacs eshell to make the terminal more l33t. The team was delighted to see my emacs performance -- splitting the editor into nested panes and running different modes. I was tickled that I got emacs into a block buster movie."
21:46:31 <elliott> http://jtnimoy-public.s3-website-us-east-1.amazonaws.com/178/TRON_GFX_BR_07.JPG
21:46:39 <elliott> how far in the future is tron set
21:46:41 <elliott> because what i am seeing is:
21:46:43 <elliott> udev is never going to die
21:48:43 -!- augur has quit (Remote host closed the connection).
21:56:30 -!- olsner has joined.
22:12:07 <elliott> topipidpiaidpiapidpipiapidpiapidapidpipipidapidapidpiapidapidpiadadaapdiapidpia
22:20:44 <elliott> cpressey: you will love this
22:20:53 <elliott> `run python -c "print 'test'"
22:21:04 <elliott> `run python -c "True = False; print True; print True is False"
22:21:10 <elliott> `run python -c "True = False; print True; print True is False; print (True is False) is True"
22:22:18 -!- marchdown_ has joined.
22:24:34 -!- marchdown has quit (Ping timeout: 276 seconds).
22:24:35 -!- marchdown_ has changed nick to marchdown.
22:28:35 <elliott> that sounds exactly as awkward as the idea of mutable constants is
22:31:09 <elliott> ais523: please tell me that works
22:31:16 <ais523> elliott: it requires -v
22:31:22 <elliott> what does -v do again? extensions?
22:31:27 <ais523> no, it just lets you do tha
22:31:37 <ais523> I thought that letting people do it by accident was too mean
22:31:57 <cpressey> nothing that happens in INTERCAL is ever an accident
22:31:58 <ais523> in CLC-INTERCAL, you have to write it indirectly, as in DO .1 <- #2 DO .1 <- .1/#1
22:32:19 <ais523> that's a simple example, but in general it can be hard to spot you're assigning to a constant in more complex programs
22:33:05 -!- cpressey has quit (Quit: /catch sufficiently not mephitic solidity).
22:33:10 <ais523> so I put it behind an option for safety reasons
22:36:10 <ais523> also for portability, DO #1 <- #2 is a syntax error in INTERCAL-72, and thus might be being used for its properties as a syntax error
22:36:21 <ais523> and the switch chooses whether it compiles as a syntax error or a calculate statement
22:40:28 -!- zzo38 has joined.
22:40:30 <elliott> heh, it's literally impossible to extend INTERCAL
22:40:44 <elliott> you can extend most languages safely by making a previously-invalid construct valid
22:40:48 <elliott> in INTERCAL, that doesn't work
22:41:16 <ais523> elliott: some extensions have been done like that
22:41:23 <ais523> e.g. threading when two COME FROMs aim at the same line
22:41:23 <elliott> ais523: but they break programs that rely on those lines to be invalid
22:41:39 <zzo38> What you can do with INTERCAL is make up where there are compiler switches to select which extensions are available
22:46:01 <ais523> CLC-INTERCAL actually uses a plugin architecture to handle thata
22:46:07 <ais523> although they're called "preloads"
22:49:27 -!- augur has joined.
22:53:45 <zzo38> Do you know what is wrong with the "TRON:Legacy" picture? Is that the control key is missing.
22:56:14 <elliott> oh, tron: legacy is set in... the present day? huh
23:00:08 -!- Sgeo_ has joined.
23:00:20 -!- wharrrgarbl has quit (Quit: Computer has gone to sleep.).
23:01:07 -!- FireFly has quit (Quit: swatted to death).
23:03:22 <zzo38> I tried to send a program to CTAN but it is not on there
23:13:39 <Sgeo_> Stanislav apparently likes Squeak
23:14:31 <Sgeo_> Sadly, there seem to be no blog posts about it
23:14:43 * Sgeo_ sees one thing that possibly tangentally mentions Smalltalk
23:16:24 -!- ZOMGMODULES has joined.
23:16:47 <Sgeo_> "The Lisp Machine (which could just as easily have been, say, a Smalltalk machine)..."
23:19:59 <Sgeo_> http://www.loper-os.org/?p=85
23:22:17 -!- ZOMGMODULES has quit (Quit: leaving).
23:22:17 -!- cheater- has joined.
23:25:12 -!- cheater00 has quit (Ping timeout: 246 seconds).
23:29:05 -!- wharrrgarbl has joined.
23:29:38 * Sgeo_ wonders how difficult it would be to make a Morphic web browser in Squeak
23:42:31 -!- oerjan has quit (Quit: Gnu tide).
23:43:53 -!- augur has quit (Remote host closed the connection).
23:46:05 <zzo38> The PDF of TUGboat 3,1 (March 1982), 10-27 is difficult to read. Where is the web source file for that article?
23:46:15 -!- augur has joined.
23:46:59 <zzo38> Maybe I should ask Knuth for a copy?
23:54:48 -!- augur has quit (Ping timeout: 246 seconds).
23:57:09 -!- zzo38 has quit (Remote host closed the connection).