00:00:45 Smalltalk at: #One put: 1. 00:09:00 -!- augur has joined. 00:10:39 Smalltalk globals keysAndValuesDo: [:key :value | 00:10:39 (value class class = Metaclass) ifFalse: [ 00:10:39 Transcript cr. 00:10:39 Transcript show: key]] 00:10:54 May have some false positives 00:14:29 In my image, there are 16. 00:15:12 I seem to have many more than 16 00:15:26 Some of them are traits. 00:15:29 Which are like classes. 00:15:35 -!- sftp has quit (Remote host closed the connection). 00:15:38 -!- sftp_ has joined. 00:15:54 Ooh 00:16:10 Optimist, Sensor, SystemOrganization, World, Display, ActiveEvent, TextConstants, Smalltalk, Processor, ScheduledControllers, Transcript, SourceFiles, ActiveHand, ActiveWorld, Undeclared, ImageImports. 00:16:22 ActiveWorld! 00:16:28 :P 00:16:43 I don't have Optimist 00:16:52 Optimist is strange. It's a True. 00:17:13 In fact, it's 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 ActiveWorld! <-- different one I suspect 00:35:54 Optimist is strange. It's a True. <-- Pessimist should be False then? 00:37:50 It should be, but it isn't. 00:57:14 So, what uses Optimist? 00:57:19 Is it possible to determine? 01:09:13 Hm, let me see. 01:10:14 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 Or you could replace Optimist with an object that pretends to be true but logs all its accesses. 01:11:08 tvvl: bot 01:11:08 nil 01:11:28 tvvl: Smalltalk globals remove: #Smalltalk 01:11:37 >.> 01:11:47 No worries, this bot is supposed to be abused. 01:11:50 I'm sure I had something more creative in mind 01:11:53 It's not *made* to be abused, but it's supposed to be. :P 01:11:56 tvvl: bot 01:12:13 It looks like that expression is simply an error. 01:12:22 The image is still working perfectly. 01:12:45 I suggest "Smalltalk globals at: #Smalltalk put: nil". 01:12:47 -!- tswettbot-boxed- has joined. 01:13:01 I'll see what that does. 01:13:03 tvvl: Smalltalk globals at: #Smalltalk put: nil 01:13:04 nil 01:13:12 tvvl: Smalltalk 01:13:12 -!- tswettbot-boxed has quit (Remote host closed the connection). 01:13:28 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 Feel free to repair the bot through IRC. :P 01:15:17 You just need to fix a certain method. 01:16:10 tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) methodSourceString 01:16:22 Oh, that's not how that works. 01:16:27 I dismiss you, tswettbot. 01:16:30 * tswett shrugs. 01:16:35 -!- tswettbot-boxed has quit (Remote host closed the connection). 01:16:51 -!- tswettbot-boxed- has joined. 01:17:08 tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource 01:17:09 bot: t1 heard: t2 01:17:27 Of course it sends every line of that as a separate IRC command. 01:17:51 Zbasu? 01:17:57 * Sgeo is confused 01:18:00 Yep, that's the name of the project. 01:19:58 tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource withBlanksCondensed 01:19:58 bot: t1 heard: t2 | t3 t4 | 01:20:12 Not much help. 01:22:58 tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource onlyLetters 01:22:58 bottheardtttTranscriptshowRCVDtcrtbeginsWithPINGifTruetsendMessagePONGtincludesSubStringIdismissyoutswettbotifTruetquitttvvlttfindStringttifFalsetsendMessagePRIVMSGesotericCompilerevaluatetallButFirsttsizetnotifyingnilloggedfalseasString 01:23:02 :P 01:24:59 tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource select: [:x | x ~= Character cr and: [x ~= Character lf]] 01:25:00 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 tvvl: (ZbasuDefaultHandler methodDictionary at: #bot:heard:) getSource select: [:x | ({Character cr. Character lf. Character tab} includes: x) not] 01:27:35 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 There, there's your source code. :P 01:28:26 Oh, interesting. All the argument names are absent. 01:29:13 All the argument names in the entire image. And there are no comments. 01:29:24 I'm guessing that's supposed to happen when the sources file can't be found. 01:37:52 -!- lament has joined. 01:43:29 eir 01:52:13 coppro: I know, i know. 01:52:17 s/i/I/ 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 augur: you always join but never leave, how is that possible 02:43:35 lolwut 02:49:44 -!- lament has quit (Ping timeout: 248 seconds). 02:51:14 augur: i've just never noticed you leave 02:51:24 you're not paying attention then! 02:51:26 yay complexity theory has been discussed here 02:51:51 oh i thought you had done some sorta magix 02:52:37 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 sparse = for some polynomial p there are at most p(n) words of length n in the language 02:54:56 oklopol: even worse, if there's unary languages that are NP-complete, P=NP 02:55:16 Zwaarddijk: i'm actually just now writing the proof of that 02:55:36 cool 02:55:42 care to share it once it's done? 02:56:13 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 yes i was writing it for your pleasure 02:56:36 but that was kinda simplified 02:56:43 i'll be happy to get into the details ofc 02:57:56 you need an SAT encoding where setting a value to true or false doesn't increase its length 02:58:20 ahm 02:58:22 then let p be a polynomial such that the reduction from SAT to the tally set takes time at most p 02:59:05 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 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 that should be the key points 03:00:49 is it followable? 03:01:00 kind of a random list of facts 03:01:33 hm, yeah I get the gist of it 03:01:45 I was thinking, btw, how would a language like 03:02:19 1^(R(x,y), x and y being any integer, and R() being the Ramsey numbers 03:02:22 be classed? 03:02:45 R(x,y) is very difficult to compute, but is that even relevant to the language itself? 03:03:33 i'm sure no one knows a fast algorithm for that because R(5,5) is open 03:03:40 exactly 03:03:42 it's 43-49 iirc 03:03:47 does this mean that language is difficult 03:03:50 oklopol: ever played with agda? 03:03:53 too? 03:04:53 Zwaarddijk: even though tally sets cannot be NP-complete, they can be exponential time or even uncomputable 03:05:05 oh wait 03:05:16 we don't know ... 03:05:16 there was something about NP-hardness 03:05:29 oh well we certainly know they can be uncomputable 03:05:36 that's trivial 03:05:52 well, the NP-completeness is unknown, that was my point 03:06:07 erm okay it seems that 03:06:18 does P=NP => NP-complete tally sets, or is it just NP-complete tally sets => P=NP? 03:06:35 if P=NP, then {1} is MP-complete 03:07:25 but my ct books says tally sets cannot be even bounded truth table hard for NP 03:07:43 i guess that's essentially the same thing 03:08:05 erm 03:08:08 when I read the thing about tally sets first 03:08:15 I figured that's pretty much proof that P!=NP 03:08:46 or maybe at least the closest we have? 03:09:04 erm the reason i gave the proof is that it's a simple little thingie 03:09:25 sparse NP-complete => P=NP is much more interesting 03:09:57 yeah, I figured that much 03:10:29 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 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:06 augur: no 03:11:17 oklopol: you should 03:11:18 its fun 03:11:29 i'm sure it is 03:12:08 but umm, i should go to work 03:12:38 I have recently realized I should learn javascript :| 03:16:32 Muahahahaha 03:18:28 :| 03:18:36 yes, it is a terrible thing to realize 03:23:46 http://sss.cs.purdue.edu/projects/dynjs/javascript_the_evil_parts.png <-- recommended book to learn from 03:26:00 got it already! 03:26:26 (not really) 03:29:46 oklopol: you do math, right? 03:29:49 Gregor! 03:30:41 augur: I don't do math :P 03:30:46 not you 03:30:51 im just saying hi to you 03:31:01 No, you're saying "Gregor!" to me. 03:31:07 Durpadoopadlip 03:31:20 -!- copumpkin has quit (Quit: Computer has gone to sleep.). 03:31:21 augur: yes 03:31:52 Gregor: yes, thats a way of saying hi 03:31:56 oklopol: well, you can do math in agda! 03:32:04 i can but umm. 03:32:04 for instance, im doing abstract algebra right now! 03:32:11 You can do math in JavaScript too X-P 03:32:16 Gregor: i mean proofs 03:32:17 what's abstract algebra, is it universal algebra? 03:32:27 augur: And I mean to trollolol :P 03:32:36 oklopol: eh. in this case its just some graph-theoretic stuff i guess? 03:32:41 i dont know 03:33:08 okay 03:33:19 must be pretty damn abstract if you don't know what it is 03:34:16 according to wp, abstract algebra is the same as universal algebra 03:34:24 augur: I didn't get libc.so *sobblecopter* 03:34:47 Gregor: sux4u 03:34:47 -!- sebbu has joined. 03:35:28 augur: Why even say "hi" if I can't then relate personal tragedy :P 03:35:30 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:36:27 Gregor: courtesy 03:36:34 oklopol: hardly! 03:37:29 currently im proving that any graph order built from Unit and disjunctive concatenation will be a linear order 03:37:42 disjunctive concatenation? 03:38:56 -!- sebbu2 has quit (Ping timeout: 276 seconds). 03:38:57 concatenation with disjoint union of the underlying sets 03:39:20 and how do you "concatenate" graphs 03:39:27 good question! 03:39:37 in this case, its roughly like so 03:41:38 (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 plus the relevant isomorphism to make the new relation be of type (X + Y) x (X + Y) -> Bool 03:42:12 so connect vertices of X to those of Y 03:42:13 roughly speaking 03:42:27 right, the X's point to the Y's 03:42:29 exclusively 03:42:39 well obviously that's a total order 03:42:44 nope 03:42:48 the X's dont point to themselves 03:42:52 total orders are reflexive 03:42:58 linear orders are irreflexive 03:43:04 i mean, it COULD be total 03:43:05 or linear 03:43:25 depending on whether you state from (1, const True) or (1, const False) 03:43:34 the former is a total order, the latter is a linear order 03:43:40 well okay linear, point is that's obvious, easier than 1+1=2 03:43:58 perhaps! depends on how you define 1, 2, and + :) 03:44:00 and =! 03:44:11 but its neat cause ive got a _proof_ 03:44:12 almost 03:44:25 im still constructing the proof that (1, const False) is a linear order 03:44:30 it's NEAT, but it's not math 03:44:43 well it's math but it's kidss math 03:44:46 *kids' 03:45:22 :( 03:45:26 true 03:45:35 but you can do growed up math too! 03:45:39 im just not doing that kind of math 03:45:45 because its not relevant to my work 03:45:48 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:06 well whatever :| 03:46:21 i'm on a course about formal proving 03:46:24 but we use HOL 03:46:57 hopefully i'll be able to prove that same theorem in a month or so 03:47:01 i doubt i could do it now 03:48:39 okay gotta go -> 03:50:19 see ya oklopol 03:50:20 * augur bites oklopol 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:43 Ah, usenet: 08:34:44 Newsgroups: sci.math,comp.theory,sci.logic,comp.lang.c,alt.religion.christianity 08:34:44 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 quite esoteric - http://arxiv.org/abs/1104.0924v1 09:08:36 -!- oerjan has quit (Quit: leaving). 09:30:16 Newsgroups: sci.math,comp.theory,sci.logic,comp.lang.c,alt.religion.christianity <-- that's a joke, right? 09:30:48 I mean, that list... 09:31:04 fizzie, or was that not a To list for one message? 09:31:30 There's no "To:" header in postings; but it was a Newsgroups: header for one (crossposted) message, yes. 09:31:59 I mean, it does have both "computer code" and "robot jesus" in the subject, why not. 09:32:57 The contents didn't really make sense, though: http://groups.google.com/group/comp.lang.c/msg/5e1c4335efdc2ecf 09:33:01 (How surprising.) 09:42:39 fizzie, looks like program code 09:42:52 fizzie, probably in R as it said in the subject 09:43:01 The syntax looks like R, yes. 09:43:09 Well, except those quotation bits. 09:43:11 I don't know R however. 09:43:31 fizzie, could be some sort of comment? I don't know 09:43:41 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 it could be doing the intercal way. Invalid syntax = comment 09:44:12 iirc 09:44:15 R comments are from # to end-of-line. 09:44:21 ah 09:46:07 The same author posted a P=NP "proof" the other day, too. 09:46:47 ah.. 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 ,[->+>+<<]>>[<<+>>-]>+>>++++++[<<[>++<-]>[<+++++>-]>-]<<[->+>+<<]>>[<<+>>-]>>+<<<<[>>>>>>>>>>>[-]+[<<<<<<<<<<<<<[->>>>>>>>+<<<<<<<<]>>>[->>>>>>+<<<<<<]<[->+>+<<]>>[<<+>>-]>>>>[>[-<->>>+<]<<]<[>]>[-<<<<<<<<+>>>>>>>>]>[-]>>>+<[-<<<<<<<<->>>>>>>>]<<<<<<<<[[-]>>>>>>>>>->-<<<<<<<<<<]<[->+>+<<]>>[<<+>>-]>>>>>>>>>]<[->>+>+<<<]++++++[->>++++++++<<]>>.[-]>[-<<<<<<<<<<<<[-]<[->+>+<<]>>[<<+>>-]<[->>>>>>>>>>>>>+<<<<<<<<<<<<<]>>>>>>>>>>>>]>[ 11:50:28 oh hey, bf joust 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 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 anyone familiar with brainfuck? <-- yes, to some degree 12:04:09 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 (of course it is probably possible to obfuscate code in many languages to get that effect there too) 12:06:46 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 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 Ilari, what mailing list heh? 12:33:27 Well, basically one mailing list was shut down and new one created to continue (apparently mailman can't rename mailing lists). 12:33:42 ah 12:33:46 well that makes sense then 12:33:50 And the admins copied the subscriber lists. 12:33:54 (well, mailmail doesn't) 12:34:33 All data wasn't copied. The password changed for instance. 12:35:09 ouch 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 R-Type! You survived the night! 14:36:25 * R-Type scowls at cpressey 14:36:45 I credit your good attitude. 14:39:09 -!- Sgeo has quit (Ping timeout: 246 seconds). 14:43:18 -!- wareya_ has changed nick to wareya. 14:54:48 cpressey, hm, why did you make the bot act like that? Is it a reference I'm missing or something? 15:01:55 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:01:55 * R-Type groans 15:02:33 cpressey, I think that got cut off 15:02:39 "So I modelled its personality after a cat I met o" 15:02:49 So I modelled its personality after a cat I met once. 15:02:53 ah 15:03:03 I guess a rather annoying cat... 15:04:08 It was a stray that was rescued. It was also a longhair. 15:04:46 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 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:07:36 ah 15:08:00 cpressey, I don't know R though 15:08:02 -!- Phantom_Hoover has joined. 15:09:47 Vorpal: you don't have to know it to appreciate how BEAUTIFUL it is. 15:10:02 See the beauty! http://pastie.org/1768075 15:10:43 The command line to run it, alone, is worth it. 15:10:46 hm 15:11:00 "irc.irc.irc" is the greatest hostname ever. 15:11:28 cpressey, if you want to avoid the erlang shell you can get pretty silly command lines there too 15:12:23 "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 "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:13:11 That's better, actually. 15:14:21 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:14:40 Very rarely nowadays. 15:14:52 And the misses are cringeworthy. 15:14:55 What's xkcd? 15:15:06 Oh, I apologize for that. 15:15:15 cpressey, a Thing Man Was Not Meant To Know. 15:15:47 the master xkcd will rise from the sunken city of frwgll 15:15:51 I know as much about xkcd as I want to -- more, actually. I should not tempt fate. Or #esoteric. 15:15:55 (That's Welsh.) 15:16:50 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 http://www.xkcd.com/879/ <<< i like this one 15:17:49 -!- pumpkin has changed nick to wharrrgarbl. 15:18:05 http://www.xkcd.com/881/ <<< and could someone explain this to me 15:18:12 Vorpal: Depending on who you ask, it is THE webcomic. 15:18:18 is the joke that they have a weird way of hugging 15:18:49 cpressey, it was THE webcomic before ~400 or so. 15:20:20 but i suppose it's still the simpsons of webcomics 15:21:04 Once again oklothink triumphs. 15:21:28 err... sure? now can you explain 881 to me 15:21:35 is it about his illness? 15:22:32 It's about LOOK AT ME I CAN WRITE CRINGEWORTHILY AWFUL "EMOTIONAL" COMICS WITH SCIENCE SHOEHORNED IN I AM NERD HUMOUR 15:22:55 I am fascinatingly tempted to actually look at it. 15:23:12 Also *anyone* who thinks probability is worth doing for practical applications should be shot. 15:23:28 are you sure there isn't some sort of punchline? 15:23:43 what are the numbers in the table 15:23:51 The impression I get is that the actual *mathematics* requires some kind of degree. 15:23:56 *to understand 15:24:10 like, that many survive 5/10 years of X 15:25:03 and i wonder if the way they hug is relevant 15:25:26 You're overanalysing it. 15:25:57 i think i just don't get it 15:26:05 Perhaps if I prepare myself mentally and emotionally beforehand sufficiently, I can look at it. 15:26:19 cpressey: i would appreciate that 15:26:36 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 fun little problem: find a 5-regular planar graph, where 5-regular = every vertex has degree 5 15:26:43 oklopol, I think you're assuming there's an actual joke somewhere under the mawkish sentimentalism, and are combing through it. 15:26:50 *for anything funny. 15:26:54 OK, here goes. 15:26:56 well yes 15:27:42 um 15:27:53 cpressey, you shouldn't have done it. 15:28:00 Phantom_Hoover: You are correct in that. 15:28:23 Well, unless you have the love for your fellow humans of Charlie Brooker. 15:28:56 I don't know who that is and the extra information is not helping me recover. 15:29:16 Charlie Brooker is an infamously misanthropic reviewer of things. 15:29:21 i suppose this is the right time to tell cpressey that santa isn't real 15:29:28 OK, well: oklopol, if you want my opinion: it wasn't intended to be funny. 15:29:47 It was intended to be Hallmark-y. 15:30:02 For lack of a better adjective. 15:30:15 -!- impomatic has joined. 15:30:54 "mawkish sentamentalism", I suppose that's a good way to put it too 15:31:06 but 15:33:05 oklopol: this was all a PLOT by you, to get me to read an xkcd, WASN'T IT 15:33:29 cleverly FEIGNING non-understanding of the fail 15:33:51 hm, or can you actually call that fail? because i'm sure it was totally what was intended 15:34:13 i wouldn't know, I DON'T GET IT 15:34:19 oklopol: THERE IS NOTHING TO GET 15:34:24 MUST BE 15:34:58 oklopol: Are you familiar with a pre-web comic strip called Fred Bassett? 15:35:31 Sometimes, there is nothing to get. 15:35:33 no, except if it's pre-web i might know it in finnish 15:36:19 oklopol: "Koiraskoira" 15:36:24 (the internet is amazing sometimes) 15:36:42 or "Retu, Pitko" 15:36:53 (thanks wp) 15:37:16 oh yeah i've seen those comics 15:37:21 in finnish prolly 15:37:40 "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:38:15 imo, this is the xkcd version 15:39:47 maybe i'll try to solve it tomorrow 15:39:51 too tired now 15:40:02 koiraskoira sounds really silly 15:40:13 retu i may have heard 15:40:22 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:40:24 koiraskoira = male dog 15:41:05 well you can always just make a play on words 15:41:27 never funny, but good enough for a newspaper comic strip. 15:42:14 I have this particular strip hanging in my cube: http://www.glyphjockey.com/uploaded_images/Uncanny_Old_Gags_1-772109.jpg 15:42:34 It's revenge against those who see fit to hang xkcds where others can see them. 15:43:15 i.... don't get that one either 15:43:23 have i become even stupider 15:43:44 i like it tho 15:44:35 oklopol does not know the hubris of man. 15:45:51 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:45:57 *point 15:46:17 i mean 15:46:19 something related to that 15:46:41 oh the first guy is in the picture 15:46:49 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 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 This would perhaps be justified were you Vorpal, but you are not. 15:47:25 i think i'm seeing it 15:47:34 nice puzzle 15:47:36 -!- MigoMipo has joined. 15:47:40 hmmhmm 15:47:42 The objective of dada is to freeze the brain until the dressmakers' assistants arrive. 15:48:49 cpressey, you should say to everyone "really, you don't get it? It's obvious!" 15:49:03 yeah no my approach didn't work 15:49:10 Phantom_Hoover, not every comic strip has a punchline. 15:49:23 depends a bit on which webcomic though 15:49:26 Phantom_Hoover: In my younger days... 15:50:01 has the author said there's no solution? 15:50:10 oklopol 15:50:17 cpressey 15:50:41 oklopol's use of the words "solve" and "solution" in regard to comic strips disturbs me somewhat. 15:50:51 And Vorpal performs quite possibly the most amazing feat of oblivious demonstration the world has ever seen! 15:51:49 cpressey: if you directly see why a comic is funny, you didn't learn anything. 15:51:56 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 I don't think Vorpal even reads what other people say beyond the most cursory examination. 15:52:46 Phantom_Hoover, I read the previous three lines + the highlight one 15:52:49 oklopol: that is true, although I am not always seeking to learn new things when I read a comic strip. 15:52:53 It's just tangential to the brilliance of his ego. 15:52:57 (the previous ones to the highlight that is) 15:53:09 This is particularly apparent whenever any form of subtlety is applied. 15:53:23 Phantom_Hoover, but come on... comics like freefall doesn't use a punch line in *every* strip. 15:53:26 Vorpal, are you aware that we don't know what lines your IRC client highlights? 15:53:30 cpressey: well to be honest the only reason i read comics is to take a break from thinking. 15:53:40 cpressey, " This would perhaps be justified were you Vorpal, but you are not." had my nick in it 15:53:48 pretty obvious it would highlight me 15:53:55 Sarcasm being one thing he is utterly unable to detect or penetrate. 15:55:24 Vorpal: how's uni 15:55:41 Anyway, xkcd pegged why R is the language of the future. It tells you that you're going to DIE 15:55:46 which year is this again? i have some trouble with time 15:56:09 cpressey: in 881? 15:56:24 oklopol: the sappy one with the statistics and the hugging, yes 15:56:39 well that's what i initially assumed, but the details don't quite seem to fit 15:56:45 mainly 15:56:50 Ooh, Edinburgh apparently has in international science festival. 15:56:52 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:00 ohh 15:57:13 Yay, I'm in Venice for half of it. 15:57:14 real life applications just told the reader it's about his disease 15:57:23 okay thanks 15:57:34 oklopol, and how is it for you? 15:57:52 oh, oklopol didn't get the sappy part? ok, that was a misunderstanding on my part 15:57:53 Vorpal: trying to get my first publication this week 15:57:57 otherwise not much 15:58:00 *: trying 15:58:13 erm, i mean write my first article which i will then try to get published 15:58:16 oklopol, ah. Good luck! 15:58:31 yes, the stick figure hates statistics because statistics are telling him that his friend/lover/co-stick-figure is gonna DIE 15:59:15 hm, everyone will die sooner or later 15:59:20 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 15:59:39 Vorpal: what lab? 16:00:50 There appears to be something about how the Vatican ascertains whether a miracle has occurred. 16:00:58 I want to go to that purely for the absurdity. 16:00:59 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 a chick bleeding out her vag ain't no miracle 16:01:56 My Idiot Chemistry Teacher outdid herself today. 16:02:05 i took this "theoretical" course on real-time systems and i can guarantee you that sucked more than yours ever could 16:02:24 First she complained about the idea of firing nuclear waste into space because it would become our nuclear dumping ground. 16:02:40 Y'know, because it's so easy to spoil the pristine landscape of space. 16:02:49 :D 16:03:10 isn't the sun already slightly radioactive 16:03:16 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:17 a wee bit 16:03:32 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 but i suppose it's nothing compared to whatever our nuclear plants produce 16:03:59 So I was like "actually I can—" "NO YOU CAN'T YOU'RE JUST PRETENDING" 16:04:10 Phantom_Hoover: I think I'm in love 16:05:00 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 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 whether... liquids can have... pressure... with a chemistry teacher 16:06:07 i mean, the other things, i can say, well, space, that's just not her domain 16:06:08 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 cpressey, in fairness, she confused pressure with compressibilit— wait, I'm not giving her any quarter, that's just as bad. 16:06:45 well you can just slingshot the stuff into space 16:06:47 need no rocket 16:06:54 Phantom_Hoover, that too. But even if that was solved, doing it by rockets would be far too expensive. 16:07:15 didn't the buld a rocket with a 20000 budget somewhere 16:07:17 *build 16:07:34 oklopol, 20000 of what? 16:07:38 money units 16:07:40 EUR? USD? 16:07:44 what does it matter 16:07:46 some kind of solar-powered magnetic rail 16:08:12 oklopol, hah 16:08:20 hah? 16:08:21 *railgun 16:08:27 HAH 16:08:37 Vorpal, they're all, like, within 1.5 times each other. 16:08:42 Except yen. 16:08:42 oklopol, I was referring to that 20000 SEK is a lot less than 20000 USD for example. :P 16:08:52 well right, but it's SMALLER 16:09:00 Phantom_Hoover, I believe 1 USD is about 8 SEK or such 16:09:01 but i suppose you got that already 16:09:04 Dammit where's pikhq I came up with the best Japanese joke. 16:09:05 haven't checked in a while 16:09:14 i mean 20000 is ASTRONOMICALLY LESS than what rockets usually cost 16:09:22 oklopol, indeed 16:09:25 who cares how many astronomers smaller it is 16:09:46 oklopol, any idea about how much payload it could lift? And to what orbit? 16:10:07 oh i don't know, and i'm not even sure this story is true 16:10:11 my point is mainly 16:10:30 that i doubt there's an intrinsic reason for rockets to cost a lot 16:10:50 rockets that just need to escape gravity 16:10:55 well, as I see it, it's the fuel that's expensive. thus: some kind of solar-powered magnetic railgun 16:11:08 It would probably have to be a few kilometers long, though 16:11:08 one issue with rockets is that they need to haul the fuel they need to power themselves. 16:11:18 which makes them heavier, needing more fuel 16:11:30 How long is the Forth Bridge again? 16:11:31 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 again, completely unconfirmed random data 16:11:54 cpressey, I AM TOTALLY QUALIFIED TO ANSWER THAT 16:11:54 -!- cheater00 has quit (Ping timeout: 246 seconds). 16:12:09 OH WAIT VORPAL IS HERE NO I DON'T KNOW ANYTHING ABOUT SCOTLAND I AM WELSH 16:12:34 FROM NEWPORT 16:12:39 SHEEP SHEEP SHEEP 16:12:41 Phantom_Hoover, hrrm, I think I need to check logs on where you come from :P 16:12:57 I AM TOTALLY NOT FROM THE CITY RIGHT NEXT TO THE FORTH BRIDGES 16:13:35 DUNFERMLINE 16:13:39 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:13:48 :D 16:13:53 Vorpal funny 16:14:04 cpressey, 2.5km, BtW. 16:14:12 -!- cheater00 has joined. 16:14:19 (For the rail bridge; the road bridge is longer IIRC.) 16:14:39 Phantom_Hoover: ty 16:15:04 Why? 16:15:50 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 And it could only launch relatively light things 16:16:24 And I don't know that it could get them further than orbit 16:16:25 "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 But once in orbit, they could use rockets very very effectively 16:16:41 (It's the UK body to which easily-offended people complain.) 16:16:57 cpressey, also you'd never finish painting it.* 16:16:58 cpressey, I'm not sure you would get the same maintenance cost for a railgun and a bridge though. 16:17:07 Phantom_Hoover: yeah yeah har har har 16:17:09 *they actually finished painting it a few years back 16:17:41 Vorpal: no, but, same order of magnitude, i was guessing 16:17:54 hm, I'm not qualified to answer that 16:18:00 -!- azaq23 has joined. 16:18:12 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 although, better the Gobi desert (or whereever) than all of Europe, as I think PH mentioned 16:18:55 quite. Hm how would it work? Would it be straight or would it curve upward at the end? 16:19:04 I'm not sure :) 16:19:19 If it was straight, it would have to be REALLY long 16:19:43 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 If it curves upward... that seems like it would be harder to do 16:19:51 yeah. 16:20:19 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 yeah I don't think that is the largest issue 16:21:08 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:19 of course 16:21:43 yeah, so let's build this sucker 16:21:48 when I said rockets were expensive, I meant from the surface of the earth. 16:21:50 >_< 16:22:32 I think the name 'Irn Bru' is inherently bullying. 16:23:06 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 would be good in case of accidents. 16:23:54 less risk of damage in case it doesn't reach orbit 16:24:23 I don't know. I don't see why not 16:26:08 I seem to remember there is some complication with getting into polar orbits. Hm... 16:27:55 Possibly, but the wp article doesn't suggest anything really difficult 16:28:33 ISTR polar orbits are much higher than low-earth. 16:28:48 Also you have to correct for the earth's rotation as well. 16:29:52 Actually I think the second point is the main one, particularly as rockets tend to be launched from fairly low latitudes. 16:30:29 well, if the destination is orbit, the railgun approach gives you very limited options, no matter which way it's pointing 16:30:59 UNLESS you put it on a GIANT TURNTABLE 16:31:08 ALTERNATELY: WHEELS 16:33:42 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:04 Forget those, and WHEEE 16:34:16 HMM 16:34:26 What orbit is the stuff being fired into again? 16:34:57 Uh, whatever's most conventient, if the ultimate purpose is to get spent nuclear fuel into the sun or whatever 16:35:03 *convenient 16:35:24 Low-earth seems the most obvious option, then. 16:35:35 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:06 Do it in Ecuador and fire over the Pacific.* 16:36:09 well, actually I guess along the Antarctic 16:36:10 *worst idea 16:36:44 what's the fuel consumption difference between to orbit vs shot into space? 16:36:44 Phantom_Hoover, isn't that the wrong direction too? With regards to Earth's spin... 16:37:03 or is it relative depending on what shooting means 16:37:29 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 a really elliptical orbit might be good then -- you could get out of it at the far point 16:38:00 not sure 16:38:22 oh we were still talking about completely escaping 16:38:31 cpressey, once you get far enough I suggest ITN for low energy transfer towards the sun. 16:38:33 oklopol, yeah, escape vs. orbit is pretty big. 16:38:40 i don't see why just leaving that shit on the orbit would be all that dangerous 16:39:05 Low orbits decay quite quickly. 16:39:05 (http://en.wikipedia.org/wiki/Interplanetary_Transport_Network) 16:39:38 Phantom_Hoover, so would it be better to go to orbit and then break away rather than break away directly? 16:39:50 Phantom_Hoover: so does your mom but i still keep doing her 16:40:06 no wait 16:40:08 Yes, because thrusting from orbit doesn't have the complications that it does on a planet. 16:40:09 that was a bad argument 16:40:13 here's a better one 16:40:21 i'll be dead by the time they come down so what do i care 16:40:24 Phantom_Hoover, right. 16:40:24 (I know what oko is going to say, so he needn't bother.) 16:41:09 Phantom_Hoover: erm what, thrusting your mom from orbit doesn't have the complications the it does on a planet? 16:41:26 More or less. 16:41:49 maybe in orbit, now it doesn't quite look like the correct kind of thrusting 16:42:40 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 now that it's obscure not-really-a-joke explanation day 16:44:54 but having sex weightless is one of the fundamental experiences in life 17:08:23 that's what she said 17:10:20 R-Type: goodbye 17:10:20 * R-Type scowls at cpressey 17:10:25 -!- R-Type has quit (Remote host closed the connection). 17:10:32 What does R-Type do? 17:11:08 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 So I modelled its personality after a cat I met once. 17:11:46 R-Type is a computer robot 17:12:00 oklopol, what is R-Type 17:12:11 R-Type is a computer robot 17:12:19 -!- cheater- has joined. 17:12:51 cpressey, have you played Elite 17:14:54 -!- cheater00 has quit (Ping timeout: 246 seconds). 17:15:46 Phantom_Hoover: I don't think so. That's the 3D wireframe one for the 8-bits, isn't it? 17:15:50 Yep. 17:17:42 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 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 Ilari, any idea how accurate that estimate is? 17:43:09 No idea. These processes are highly discrete and distributions behave badly. Fourth quadrant stuff for sure. 17:45:36 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:46:19 Logspace: /8.971 17:47:50 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 Longhair + living on the streets = permanent knots in fur = quite painful, I imagine = not the happiest individual. 18:24:16 um can't they cut it off... 18:27:56 like, that many survive 5/10 years of X 18:28:03 that was my guess when i read it... 18:28:17 oerjan, you read xkccd? 18:28:20 *xkcd 18:28:35 randall munroe _has_ some disease in the family 18:28:36 yes 18:29:29 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:40 ouch 18:29:43 Longhair cat? 18:29:46 -!- asiekierka has quit (Ping timeout: 240 seconds). 18:29:56 Phantom_Hoover: yes 18:30:14 What cat? 18:30:26 The cat whose personality R-Type's is modelled after. 18:30:29 R-Type cat? 18:30:45 vietnamese rolling furball 18:33:12 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 those _would_ tend to be the less damaging ones, one would think 18:33:59 except maybe someone probably has one of the worst ones just for the hell of it... 18:34:12 s/maybe // 18:34:27 he would have to constantly explain it 18:34:34 heh 18:34:58 well i mean like that infamous genitals one... 18:35:11 i don't think a comic can be stupid enough that... erm which one is that? 18:36:09 Low 600s. 18:36:10 http://xkcd.com/631/ 18:36:27 Don't think too hard about the joke in that one either. 18:37:31 interesting. 18:38:08 * oklopol tries not to think about it 18:38:42 -!- elliott has joined. 18:38:49 elliott 18:38:54 oklopol 18:39:08 fun little problem: find a 5-regular planar graph, where 5-regular = every vertex has degree 5 18:39:16 some platonic solid 18:39:48 icosahedron probably 18:39:50 06:58:51: (I am pretty sure Eliezer Yudkowsky once said "a".) 18:39:51 06:59:27: it would be rather impressive if somehow he has carefully avoided a particular common word for years without being detected. 18:39:51 i'm suspicious now 18:40:02 maybe "Eliezer Yudkowsky" is an anagram... 18:40:19 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 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 if you think about a 3d ball 18:41:09 erm 18:41:10 i mean 18:41:15 to come up with *a* solution 18:41:29 you mean there's anything simpler than an icosahedron? 18:41:33 14:57:31: elliott: but really, is PerlNomic better than another nomic we could come up with? 18:41:37 how many is icosahedron? 18:41:41 tswett: define better 18:41:41 vertices 18:41:44 20 faces 18:41:54 tswett: Is skiing better than Chess? 18:41:59 i have two constructions that give 12 + 4k vertices 18:42:00 for any k 18:42:01 12 vertices (it's dual to dodecahedron) 18:42:23 then your k=0 may be that 18:42:37 one of them gives some hedron as the 12 case, i don't know about the other one 18:42:44 oklopol: even real k? 18:42:52 cpressey: interestingly enough, no! 18:42:57 EVEN QUATERNIONIC 18:43:06 just complex - real works 18:43:36 EVEN TUPLE-VALUED k 18:43:39 where - is set theoretic subtraction since you're smartasses 18:45:15 tuples of small categories, that is 18:45:39 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 kind of hard to explain but maybe you'll get it 18:46:04 vey easy when drawn 18:46:13 *very 18:46:17 -!- elliott has quit (Remote host closed the connection). 18:46:34 that's equivalent to an icosahedron when k = 0 18:47:28 er what's C_5 again 18:47:32 cycle of 5 18:47:35 oh right 18:47:39 so a pentagon 18:48:06 sure 18:48:34 in this case i'm putting them on a sphere so pentagon is not really a good term 18:48:49 because the gon is gone. 18:50:08 fun little problem: find a 5-regular planar graph, where 5-regular = every vertex has degree 5 <--- wait what? 18:50:25 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 do the edges have to be straight or something? 18:50:32 maybe if i don't remember, no one will 18:50:33 ...but the faces of a dodecahedron are pentagons 18:50:57 -!- elliott has joined. 18:51:08 oerjan: if you put a C_5 around a sphere, there are no angles 18:51:20 because if not, just have two vertices, and 5 edges between them. done. planar as all hell 18:51:35 oklopol: OR ARE THERE INFINITE ANGELS 18:51:47 cpressey: using the usual definition of graph here 18:51:51 just one edge and no self-loops 18:52:18 oklopol: "just one edge"? 18:52:22 oerjan: or did you mean there can't be an isomorphism between the result of the construction and an somethinghedron? 18:52:27 cpressey: between each pair 18:52:32 oh oh oh 18:52:33 ok 18:52:44 no multigraphs or whatever they call that 18:52:51 they often call them multigraphs 18:53:03 oklopol: i'm just pointing out pentagons can be used for this, in a sense... 18:53:07 but definitions differ a lot in gt 18:53:23 although that's mixing faces and vertices with the duality 18:53:57 you can use all kinds of things if you're smart enough 18:54:29 I USE A PROJECTED PENROSE TILING FROM HYPERSPACE 18:56:02 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 no theorems needed, but a lot of definitions 18:56:53 4-critical = exists proper 4-coloring of vertices, and no 3-coloring, but in any proper subgraph there exists a 3-coloring 18:57:06 yeah no 18:57:30 wheel of order n = C_{n-1} + a node connected to each of its points 18:57:36 well that's it i guess 18:58:16 i'd rather do the what you call "kids math" 18:58:22 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 (although only slightly wrong) 18:58:36 not in agda though 19:03:33 isn't the sun already slightly radioactive 19:04:21 if by radioactive you mean "occasionally sends out enough charged particles to kill an unprotected human" 19:04:48 like, on earth? 19:05:03 no, earth is protected by its magnetic field and atmosphere 19:05:31 well i don't know any of that fancy magnet stuff but i like the idea of being protected. 19:06:08 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 I almost did it with 8 vertices, but I have one edge that goes between two vertices that already have an edge. 19:06:31 oh wait, just double this 19:06:32 which may have happened on mars 19:06:51 cpressey: double? 19:06:52 22:02:54: strsplit(gsub('^:(.*?)\\!(.*?)\\s+PRIVMSG\\s+(.*?)\\s+\\:(.*?)$', '\\1\u2603\\2\u2603\\3\u2603\\4', line, perl=TRUE), '\u2603', fixed=TRUE) 19:06:53 uh. 19:07:07 so, um, 16 vertices, which is in fact 12 + 4k when k=1! cool 19:07:21 can you describe it somehow? 19:07:40 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 22:28:22: (I've modelled its personality after a cat I met once) 19:07:51 did its eye pop out and did you eat it and absorb its esoteric powers 19:07:52 y/n? 19:08:00 q 19:08:14 ^Z 19:08:21 ? 19:08:22 ? 19:08:33 cpressey: i don't think you can do that planarly but maybe i'm mistaken 19:09:02 oklopol: it's possible i miscounted the # of edges here. maybe i'll try to draw it more neatly 19:09:14 actually it's possible planarly, if i know what you mean 19:09:15 23:08:42: 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 i don't think Vorpal quite knows what R is 19:09:30 aRray language 19:09:45 23:11:12: K is rather insane. Maybe... naw. 19:09:49 cpressey: it's probably been done :> 19:10:12 23:58:26: It annoys me that there are global constants (variables?) that aren't classes. 19:10:12 23:58:32: Transcript and Smalltalk, for example. Maybe others. 19:10:14 aren't they classes? 19:10:18 elliott: I couldn't find an implementation of K anyway. In the 4 whole seconds I spent looking 19:10:37 cpressey: Pay up, or get K3 (the cool one with the GUI thing) from a hidden subdirectory of nsl.com :) 19:10:40 as they say, 5th second is the charm 19:10:51 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 bah, no one outside britain knows the difference anyhow 19:12:15 just strangely unpronouncible places with bagpipes and leprechauns and whiskhey 19:12:53 and green. lots of green. 19:14:00 03:31:56: oklopol: well, you can do math in agda! 19:14:11 this is to embarrassing to read 19:14:17 oklopol: i swear us dependent type guys aren't that bad 19:14:22 *so 19:14:35 whoops. oklopol: i actually have 2 multiedges. dammit 19:14:49 cpressey: took me 45 minutes to come up with a solution 19:15:02 03:35:30: 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 oklopol: does gödel's incompleteness theorem count as 1+1=2? :D 19:15:19 well, that was actually coq. 19:15:25 well maybe not quite that long but longer than oerjan's 5 seconds 19:15:32 elliott: you proved that? 19:15:50 oklopol: no, russell o'connor did: http://r6.ca/Goedel/goedel1.html 19:16:08 and was he an amateur at coq? 19:16:13 well ... no :D 19:16:15 gdel's theorem isn't all that deep 19:16:23 -!- wareya has quit (Read error: Connection reset by peer). 19:16:26 "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 > let true & false = true in true & false 19:16:42 (It's the UK body to which easily-offended people complain.) 19:16:43 Not in scope: `true'Not in scope: `false' 19:16:48 PA? 19:16:53 oklopol: penis arithmetic 19:16:57 what we need is mandatory sterilization of easily offended people. 19:16:58 erm right 19:17:30 we computed many sentences that make PA incomplete in automata theory 19:17:37 -!- wareya has joined. 19:17:45 08:57:33: quite esoteric - http://arxiv.org/abs/1104.0924v1 19:17:50 mtve: you still exist?? 19:17:57 that's what i was thinking! 19:18:05 it's not rocket science, and in any case i'm talking about what an amateur can do 19:18:06 oklopol: well this is the gödel one :P 19:18:20 oklopol: printing it before we all die is impossible though. and that is because it is a poison. 19:18:21 science facts 19:18:49 i believe that 19:20:28 > let True & False = True in True & False 19:20:29 True 19:20:43 Ah, Haskell. 19:20:46 12:32:10: Hah. I seemingly got signed up to one mailing list in "opt-out" fashion (quite understandable given the situation). 19:20:47 12:33:27: Well, basically one mailing list was shut down and new one created to continue (apparently mailman can't rename mailing lists). 19:20:53 Ilari: this wouldn't happen to be the ffmpeg/libav fiasco? 19:21:12 it wasn't a fiasco, it was an imbroglio 19:21:30 elliott: Nope. 19:22:12 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 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 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:22:38 impressively childish 19:22:56 Why did they do that, BtW? 19:24:06 Phantom_Hoover: because they didn't like how the maintainer was handling proposed patches 19:24:40 How was that? 19:24:43 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 Phantom_Hoover: I think he was rejecting patches based on what they saw as trivial grounds or something 19:27:48 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 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:31:23 pretty much 19:36:42 I am becoming more and more convinced that programming (heavily, exclusively) in Python changes the way you think for the worse. 19:38:57 cpressey: only suicide can cure you 19:38:59 DISCLAIMER: 19:39:04 Do not attempt suicide because of this line. 19:39:11 (Attempt it because of the line three lines up instead!) 19:39:38 -!- Sgeo has joined. 19:39:39 16:16:25: "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 Phantom_Hoover: well people might whack goths with irn brus 19:39:48 "HAVE A FUCKING IRN BRU" 19:39:58 BRB 19:40:04 dammit, i should stop giving ph ideas 19:40:21 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 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 it's ingenious in its stupidity 19:47:58 > let 6 > 7 = True in 6 > 7 19:47:59 True 19:48:20 cpressey really likes this part of haskell 19:49:43 so it would appear 19:49:44 yes. it is amusing. 19:50:01 It's the BEST part of Haskell. 19:50:03 > let in 5 19:50:04 5 19:50:06 also good. 19:50:36 > let in let in let in let in let in let in "let" 19:50:37 "let" 19:50:44 > let a = 5 where in a 19:50:46 5 19:50:56 * Sgeo is reading about the Maude language 19:51:09 -!- azaq23 has quit (Quit: Leaving.). 19:51:09 > let me in 4 19:51:10 : parse error on input `in' 19:51:21 > let 2+2=5 in 2+2 19:51:21 Sgeo: I never got very far with Maude 19:51:22 5 19:51:30 I... just tried to tab-complete Maude, though 19:51:42 Well, it IS a name 19:53:07 > let a | otherwise = b where in a 19:53:08 b 19:53:59 > do let; let; "hi" 19:54:01 : parse error (possibly incorrect indentation) 19:54:08 sadly missing 19:54:15 cpressey: watchoo do to http://catseye.tc/lab/robin/robin.html, i'm logreading and broken links totally destroy my flow 19:54:17 oerjan: omg that would be awesome 19:54:25 > do let in; let in; "hi" 19:54:26 : parse error on input `;' 19:54:32 let in do let; let in do let; let; "hi"; let in do let 19:54:51 > let in do let in do let in do let in "hi" 19:54:52 "hi" 19:55:02 16:22:32: I think the name 'Irn Bru' is inherently bullying. 19:55:10 cpressey: really? well i guess it's kinda cheesy 19:55:13 I GUESS YOU JUST HAVE TO GROW UP WITH IT 19:55:22 IT'S MADE IN SCOTLAND WITH GIRDERS 19:55:36 it suggests the lowest-class pronunciation in my head 19:55:50 don't know if that was intentional or what 19:55:53 cpressey: it's probably meant to 19:56:02 i don't really parse it out as, you know, iron brew 19:56:16 man it's old, 1901 19:56:45 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 . 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 cpressey: HA, YOUR PUNY COUNTRY CAN'T HANDLE SCOTTISH METAL DRINK 19:57:13 16:30:59: UNLESS you put it on a GIANT TURNTABLE 19:57:14 this is now the best idea 19:57:20 wait you mean irn bru isn't something fancy gaelic? 19:57:33 hi oerjan 19:57:37 hi channel 19:57:48 -!- ais523 has joined. 19:57:49 :D 19:57:52 hi ais523 19:58:04 ais523 cannot drink Irn Bru because he is a PANSY 19:58:36 they made irn bru technically illegal with no penalty just so ais523 couldn't drink it 19:59:07 I wouldn't drink it anyway, I don't like that sort of thing 19:59:19 PAAAAAAANNNNNNNNSSSSSSSSSYYYYYYYy 19:59:44 There's something... fun about Maude's infix operators 20:00:04 oerjan: <3 20:00:27 -!- Slereah has quit (Ping timeout: 276 seconds). 20:01:03 we need a language with non-euclidean operators 20:01:09 Yes. Yes we do. 20:01:26 As the channel's resident expert on stupid non-Euclidean things, I approve. 20:01:27 the kind Man was Not Meant to Know 20:01:59 Phantom_Hoover: i'm gonna BLOW YOUR MIND 20:02:01 Phantom_Hoover: the universe 20:02:03 Phantom_Hoover: ... 20:02:06 Phantom_Hoover: is NON-EUCLIDEAN 20:02:08 so this language should be C(noneuclidean operator)^2 20:02:20 I guess 20:04:27 elliott: fuck you :| 20:04:40 augur: :) 20:04:54 agdas pretty neat tho 20:05:26 why waste all your time proving things that would take three seconds in coq :) 20:05:29 yes. yes it does. 20:05:36 elliott: ey? 20:05:48 augur: proving things in agda is a bitch. compared to coq 20:06:33 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:40 uh 20:06:44 i dont want to have to explain the magic of coq on top of stuff 20:06:44 ITT: augur has never used coq ever 20:06:52 this is true! 20:06:56 the magic of coq? 20:07:04 -!- Slereah has joined. 20:07:07 proofs in agda == proofs in coq. coq just has tools to help you write them, and agda doesn't. 20:07:14 oh what 20:07:24 what tools does coq have? 20:07:30 proofgeneral's interface to the toplevel. 20:07:38 ill have to take a look 20:07:42 you can see all your assumptions and your current goal, plus the goals left after that 20:07:48 and undo proof steps, etc. 20:07:49 augur, also the entire tactic language. 20:07:52 that too. 20:08:03 i dont mind the agda stuff. its fun to figure out how to construct it. 20:08:08 but ill take a look at coq 20:08:11 although if he's avoiding "magic" (like agda's library isn't magic?) he might want to avoid "auto" :) 20:08:19 augur: turn on three window mode and electric terminator in proofgeneral 20:08:21 im not using much of agda 20:08:23 's library 20:08:48 you are 20:08:53 because you're using its proof combinators 20:08:58 unless you're writing proofs in direct functional style 20:09:01 which i doubt 20:09:03 oh here it is 20:09:07 (setq proof-three-window-enable t) 20:09:13 eh 20:09:15 and (setq proof-electric-terminator-enable t) 20:09:20 what do you mean in direct functional stuff 20:09:28 augur: paste a proof/lemma 20:09:33 i'll tell you whether you're using the library or not 20:09:43 (protip: if there's unicode, you are) 20:09:55 well then! 20:09:59 i use unicode a lot. 20:10:20 augur: i mean apart from the things you type. 20:10:29 o wut 20:10:31 if there are unicode things in your source file that aren't names you made up 20:10:34 you are using the stdlib 20:10:43 oh probably are 20:10:59 then that's magic. if you don't believe me, look at its source sometime. 20:11:23 http://hpaste.org/45440/syntax_crap 20:11:33 look at whats source 20:12:08 the stdlib's. why are you making this simple conversation so painful X_X 20:12:17 oh right 20:12:40 oh nice, you're actually copy-pasting the stdlib directly in. 20:12:51 not copy and pasting anything 20:12:59 welp, typical unicode agda noise :) 20:13:00 are you referring to danielsson's standard library? 20:14:00 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 i am referring to the agda standard library 20:14:16 http://www.cse.chalmers.se/~nad/listings/lib-0.5/README.html 20:14:18 so eys. 20:14:19 *yes. 20:14:57 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 without referencing some magic library off somewhere in the ether 20:15:18 or, you know, just linking to its source 20:15:29 except thats more problematic if im giving a presentation. 20:15:37 and someone asks about this or that 20:15:41 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 then i have to try and remember what the standard lib says etc etc whatever 20:15:53 i see they still noise up their code with explicit level wrangling, too 20:16:04 coq doesn't have that :) 20:16:10 hooray! 20:16:15 maybe ill use coq 20:16:16 ANYWAY 20:16:18 point is 20:16:29 i rather like the unicode and mixfix 20:16:31 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:06 h 20:26:08 hm 20:26:10 coq looks interesting 20:26:57 -!- azaq23 has joined. 20:27:02 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 i understand agda proofs -- if it type checks, youve got a proof 20:29:04 flrgbl 20:29:05 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 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 i understand agda proofs -- if it type checks, youve got a proof 20:41:13 augur: uhh, same with Coq? 20:41:37 apparently someone rewrote xmonad in Coq 20:41:39 just because they could 20:41:41 ais523: ... 20:41:46 ais523: stop being slashdot 20:41:53 (with the normal Reddit-related meaning of "apparently") 20:41:59 not even reddit had that, I've seen the posts 20:42:09 it did, I think 20:42:12 "We rewrote parts of xmonad's core algorithms in Coq to prove them correct and extracted the results to Haskell" 20:42:14 -->ais523--> 20:42:23 "Someone rewrote xmonad in Coq!" 20:42:25 "For no reason!" 20:42:37 elliott: no, Transcript and Smalltalk are not classes. 20:42:44 tswett: well, they're objects 20:42:47 elliott: perhaps! but the proofs also have all these other things 20:42:53 augur: no they don't 20:42:54 beh, it'd have been more fun if there was no reason 20:42:56 unfold f, g. destruct h. etc etc 20:42:59 augur: yes, those are tactics 20:43:04 augur: if you "Print proof_name" 20:43:06 you see the lambda form 20:43:09 oh ok 20:43:10 elliott: I define "better" as "skiing is not better than chess, nor vice versa". 20:43:13 the tactics just make proofs about 159% easier to write 20:43:33 tswett: Then I say that your question is unanswerable. 20:43:38 * tswett nods. 20:43:44 tvvl: 18 20:43:52 Nope, the bot's dead. 20:43:52 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 I'd say that both are games worth playing. 20:45:36 * tswett nods. 20:45:57 Say, elliott, would you happen to know of an implementation of a Lisp that has Smalltalk-esque orthogonal persistence? :P 20:46:25 Well, just about every Common Lisp implementation lets you save the current world. 20:46:31 But, well, Common Lisp. 20:46:44 That sounds desirable. 20:47:01 flrgbl flrbgl 20:47:43 flrgbl flrbgl shfpngr! 20:47:55 tswett: Yes, but, Common Lisp. 20:47:58 Someone rewrite skiing's core algorithms in chess to prove them better and extracted the results to xmonad. 20:48:03 cpressey: yes 20:48:08 I like the change of tense there 20:48:17 -!- Sgeo_ has joined. 20:48:44 I think all mathematics should be developed with the goal of using it in a window manager. 20:49:00 Mathematical research should follow this algorithm: 20:49:13 omg, does this mean that the singularity will manage windows for me 20:49:16 by reading my mind 20:49:22 and figuring out my desired arrangement 20:49:47 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:49:50 Repeat. 20:50:43 -!- BeholdMyGlory has quit (Remote host closed the connection). 20:56:38 This message has been translated into French. 20:57:31 whoa 20:57:42 -!- impomatic has quit (Quit: ChatZilla 0.9.86.1 [Firefox 3.5.18/20110319140258]). 20:58:20 cpressey: ce message a trad.. a francais 20:58:21 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. 20:58:22 x.x 20:58:28 Suffice to say it's different in everything. 20:58:30 YAY CL 20:58:53 Doesn't CCL have it? 21:06:19 Dunno. 21:06:28 Not under the same name as SBCL, that's for sure. 21:07:44 I hope to never, ever program anything in that language. 21:08:51 -!- Sgeo_ has quit (Ping timeout: 260 seconds). 21:10:47 cpressey: Err, what, Lisp? 21:13:28 cpressey: Better experience than 99% of languages... 21:16:49 Well, Common Lisp specifically. 21:17:09 cpressey: I stand by my statement :) 21:17:50 cpressey: Admittedly the modern /environments/ aren't so ideal. 21:18:09 But the language itself is something I'd much rather have to code in than almost every other language. 21:18:14 (There are maybe ten exceptions.) 21:18:20 LIST THEM 21:18:38 Epigram 2 doesn't count due to not existing in any meaningful way. 21:19:03 Haskell is one! 21:19:13 And the others? 21:19:30 I DIDN'T MAKE A LIST 21:21:42 too few languages to warrant making a list 21:22:10 anyway, EVERYTHING SUCKS 21:22:30 olsner: you're either mocking me perfectly, or are a man I can relate to. 21:22:37 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 As long as Scheme is one of the exceptions, it kind of wins out, for me. 21:23:05 definitely not a list 21:23:18 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 cpressey: And, sure, but, Common Lisp or PHP? 21:23:39 Common Lisp or Python? Perl? C? Ada? 21:23:39 elliott: Pharen! 21:23:42 COBOL? 21:23:55 cpressey: I... am floored that you know what Pharen is. 21:24:01 Even I had to Google it. 21:24:11 phar out man 21:24:17 I heard [about it] through the grapevine 21:24:23 er, *[about] 21:24:23 "a compiler that takes a Lisp-like language and turns it into PHP" :/ 21:24:32 cpressey: was just about to correct you BRO 21:24:39 ... C++? Arc? 21:24:43 Prolog? 21:25:04 I mean, 90% of languages are really bad. 21:25:16 9% of the rest are tolerable but not any good. 21:25:27 I'd say Common Lisp almost certainly belongs to the remaining 1%. 21:25:31 *90% of the rest 21:25:34 I would totally program in C for fun before I would program in Common Lisp for fun. 21:25:58 cpressey: I don't really see how you could place Scheme above 'em but CL below C. 21:26:12 Sure, the multiple namespaces is a bit crappy, and a lot of the standard names suck but... it's still Lisp 21:26:30 Also CLOS. 21:26:48 Well, right, CLOS is one of the two tolerable OOP systems out there :) 21:29:03 elliott: I qualified my statement with "for fun" -- I am not concocting an absolute total order here. 21:29:48 I mean, dude. I just wrote a bot in R. 21:29:48 Confound your imprecision! 21:29:59 -!- MigoMipo has quit (Read error: Connection reset by peer). 21:30:04 Do I put R above Common Lisp? Apparently! 21:32:07 right now I have to debug Javascript :( not by choice obv 21:33:25 cpressey: HAVE FUN DUDE 21:34:03 Y U PUT BUG IN PROGRAM? well, now you get to take it out... 21:34:11 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 cpressey: ONLY KINSHIP WITH BRENDAN EICH CAN SAVE YOU 21:34:44 cpressey, have I mentioned the time my school told everyone to use IE 5 *for Mac* to run JS. 21:35:07 Phantom_Hoover: yes. olsner: Django. (no further words are needed) 21:35:30 Phantom_Hoover: Actually IE 5 for Mac was an okay browser. 21:35:33 It shared no code with the Windows version. 21:35:54 Indeed, but this was *last year*. 21:35:56 cpressey: listen to Django Reinhardt while doing it, it'll be SO IRONIC (hipster for "worthwhile, validating experience") 21:36:01 On computers *with Safari installed.* 21:36:10 Phantom_Hoover: :D 21:36:18 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 django is named after a person? 21:38:23 thought it would be a giraffe or something 21:40:37 :D 21:40:43 `addquote django is named after a person? thought it would be a giraffe or something 21:40:46 353) django is named after a person? thought it would be a giraffe or something 21:42:17 * Phantom_Hoover → sleep 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 "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 http://jtnimoy-public.s3-website-us-east-1.amazonaws.com/178/TRON_GFX_BR_07.JPG 21:46:34 OH DEAR GOD 21:46:39 how far in the future is tron set 21:46:41 because what i am seeing is: 21:46:43 udev is never going to die 21:46:47 (tron legacy that is) 21:48:43 -!- augur has quit (Remote host closed the connection). 21:56:30 -!- olsner has joined. 22:12:07 topipidpiaidpiapidpipiapidpiapidapidpipipidapidapidpiapidapidpiadadaapdiapidpia 22:12:41 elliott: obviously! 22:12:54 oerjan: tapodpiapotpi 22:13:09 maybe. 22:20:44 cpressey: you will love this 22:20:47 !python print 'test' 22:20:53 `run python -c "print 'test'" 22:20:55 test 22:21:04 `run python -c "True = False; print True; print True is False" 22:21:06 False \ True 22:21:10 `run python -c "True = False; print True; print True is False; print (True is False) is True" 22:21:12 False \ True \ False 22:21:15 cpressey: ^ 22:22:18 -!- marchdown_ has joined. 22:22:30 marchdown: no, march up 22:24:34 -!- marchdown has quit (Ping timeout: 276 seconds). 22:24:35 -!- marchdown_ has changed nick to marchdown. 22:24:38 THAT'S RIGHT 22:27:47 elliott: yep 22:28:05 mutable boolean constants 22:28:22 mutabonstants 22:28:35 that sounds exactly as awkward as the idea of mutable constants is 22:30:55 DO #1 <- #2 22:31:09 ais523: please tell me that works 22:31:16 elliott: it requires -v 22:31:22 what does -v do again? extensions? 22:31:23 but works 22:31:27 no, it just lets you do tha 22:31:29 *that 22:31:37 I thought that letting people do it by accident was too mean 22:31:57 nothing that happens in INTERCAL is ever an accident 22:31:58 in CLC-INTERCAL, you have to write it indirectly, as in DO .1 <- #2 DO .1 <- .1/#1 22:32:19 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 so I put it behind an option for safety reasons 22:36:10 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 and the switch chooses whether it compiles as a syntax error or a calculate statement 22:40:28 -!- zzo38 has joined. 22:40:30 heh, it's literally impossible to extend INTERCAL 22:40:44 you can extend most languages safely by making a previously-invalid construct valid 22:40:48 in INTERCAL, that doesn't work 22:41:16 elliott: some extensions have been done like that 22:41:23 e.g. threading when two COME FROMs aim at the same line 22:41:23 ais523: but they break programs that rely on those lines to be invalid 22:41:29 indeed 22:41:39 What you can do with INTERCAL is make up where there are compiler switches to select which extensions are available 22:46:01 CLC-INTERCAL actually uses a plugin architecture to handle thata 22:46:03 *that 22:46:07 although they're called "preloads" 22:49:27 -!- augur has joined. 22:53:45 Do you know what is wrong with the "TRON:Legacy" picture? Is that the control key is missing. 22:55:44 noted 22:56:14 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 I tried to send a program to CTAN but it is not on there 23:13:39 Stanislav apparently likes Squeak 23:14:31 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 "The Lisp Machine (which could just as easily have been, say, a Smalltalk machine)..." 23:16:49 how boring 23:16:59 oh yes just as easily 23:18:28 Common Lisp = Arc = Clojure 23:18:43 = Guile 23:18:48 = EMACS 23:19:12 = Smalltalk * 0.910071 23:19:59 http://www.loper-os.org/?p=85 23:20:19 no 23:22:12 GRAAAAAAHHHHHHH hi 23:22:14 well bye 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:31:54 w 23:32:36 ? 23:42:31 -!- oerjan has quit (Quit: Gnu tide). 23:43:53 -!- augur has quit (Remote host closed the connection). 23:46:05 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 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).