00:38:36 So I'm no longer totally convinced that every Turing machine either halts or does not halt. 00:38:44 Maybe Goldbach's conjecture doesn't have a truth value. 00:40:03 well definitely there is a TM where ZFC can't prove it halts or doesn't, unless ZFC is inconsistent 00:40:11 Right. 00:40:24 It seems to me that a Turing machine must either halts or does not halt (maybe I am wrong); I made a sequent calculus of Turing machine so it halts if and only if it is provable, I think (unless I made a mistake). 00:40:28 zfc, more like sucksfc 00:40:50 and likewise for whatever other formal logic you want to use to talk about turing machines 00:40:58 All the cool kids work in linear logic with no axioms. 00:41:00 zfc38 00:41:11 i would use that axiom system 00:41:28 ZFC 98 00:41:29 Different kind of logic are useful for different things. 00:41:35 Suddenly I feel like there's a topology here. 00:43:22 The singleton set {X} is closed if and only if ZFC proves that X halts or that X does not halt. 00:43:52 So is that how it works? 00:44:09 Well, I certainly haven't defined the entire topology yet. 00:44:10 well boolean algebras have Stone spaces 00:44:26 and this relates logic and topology somehow 00:44:38 too bad i know only a little logic and no topology 00:44:49 It is possible to prove that a Turing machine halts if and only if it does halt, but this isn't the case with not halting. 00:45:21 Is there linear logic with no axioms? 00:45:26 You're saying that "for all Turing machines X, X does not halt if and only if X does not halt" is not provable? 00:45:33 I should say "linear logic with no additional axioms". 00:45:43 O, OK. 00:46:08 "In mathematics, Stone's representation theorem for Boolean algebras states that every Boolean algebra is isomorphic to a field of sets." No shit? 00:46:15 tswett: No, I am just saying that it isn't necessarily provable if it doesn't halt. Sometimes it may be. 00:46:23 Oh, that. 00:46:37 tswett, have you seen the pidgeonhole principle? 00:47:12 zzo38: In Potion of Confusing, the message says "All of the objects (except one) are what they seem; there are no secret objects or fake wall or anything like that." 00:47:19 zzo38: Shouldn't that say "fake walls"? 00:47:59 shachaf: I suppose that would work too. 00:48:38 Note that "what they seem" is according to MegaZeux; if you don't know much about MegaZeux then this message probably won't help much. (MegaZeux is open source though, so that might help a bit.) 00:48:48 zzo38: I think "fake wall" is iggrammatical. 00:55:06 I don't intend to fix it right now (although you can fix it if you want to). 00:55:38 'patches welcome' 00:56:31 kmc: I like the thing where someone asks for help with their program and someone suggests a bunch of ways to improve it and they respond with "patches welcome". 00:56:53 Maybe I might fix it later, though. 00:57:02 Such as, when I continue to work on that game and add more levels. 00:57:17 e.g. http://www.reddit.com/r/haskell/comments/1gdh5u/help_tracking_down_a_possible_memory_leak_in/ 00:57:37 heh 00:58:02 kmc: should i give up on the punctuation for "eg, ie, etc", etc. 00:58:02 that's just... that specific person 00:58:04 "you should use DevURandom instead of DevRandom, unless you want to wait a long time for cryptographically secure genetic results" 00:58:07 sigh 00:58:19 really questionable that /dev/random should exist 00:58:57 in typical configurations urandom is *cryptographically* unpredictable 00:59:01 it works differently on different OSs, doesn't it? like I remember reading that BSD's "random" was actually a PRNG seeded by a guaranteed-safe amount of entropy 00:59:02 it's not information-theoretically unpredictable 00:59:13 kmc: where else will i dump my spare entropy hth 01:00:11 kmc: i think i heard that /dev/urandom is even better than /dev/random for cryptography for reasons other than speed 01:00:14 but i didn't understand the reasons 01:00:22 all you need is like 256 bits of entropy at startup and you can generate cryptographically secure random numbers indefinitely 01:00:38 for basically the same reason that you can encrypt arbitrarily long things with AES using a 256 bit key 01:00:42 except that's probably not /really/ true 01:01:18 and i mean 'indefinitely' in a practical sense 01:01:26 can you use aes in ctr mode as a good rng 01:01:34 i should think so 01:01:43 otherwise it's not a v. good stream cipher 01:01:48 right 01:01:49 but i might be missing something 01:01:50 well, would it be slow 01:01:54 right 01:02:05 Linux urandom uses some cryptographic hashing instead 01:02:06 isn't it typically, like N bits of PRNG seed gets you ~2^N bits of output? 01:02:11 well, like, safe output 01:03:13 non-cryptographic PRNGs like Mersenne Twister or MWC256 have a much larger internal state, but I think that's because they need to be fast and can't do much mixing on each output 01:03:28 in fact MT has a more expensive step that happens each n words where n words is also the state size 01:04:22 Is there a reason to use a non-cryptographic PRNG except in special cases? 01:04:29 speeeeeeeeeeeeed 01:04:40 needing a bunch of random numbers quickly isn't that special of a case, to me 01:04:46 does anyone happen to use zsh 01:05:01 but I do think that language builtin RNGs should err on the side of cryptographic strength 01:05:12 By "special" I meant "non-default". 01:05:24 ok then 01:05:28 And my question was really mostly about speed. Are cryptographic PRNGs that much slower? 01:05:39 of course now we have like, RDRAND, soooo 01:05:54 "On a i5-3210M (2.5GHz) Ivybridge (2 cores, 4 threads) I get a peak of ~99.6 million 64 bit rdrands per second with 4 threads which equates to ~6.374 billion bits per second. Not bad at all." wow 01:06:06 Well, I used ARCFOUR in Famicom Hangman, which works fine, even though that is a very slow computer! 01:06:21 I like that Python has random.SystemRandom() which is an object with the same API as the random module itself, and using urandom 01:06:26 but it would be even better if they were swapped 01:06:36 zzo38: did you drop the first several thousand outputs? 01:06:51 I wonder if that will finally get rid of the /dev/random seeding problem. 01:06:56 kmc: It will automatically do that if you don't put the space bar immediately as soon as you turn it on. 01:07:42 ok 01:07:47 -!- Sgeo has quit (Read error: Connection reset by peer). 01:07:53 * kmc makes plans to cheat at Famicom Hangman using RC4 biases 01:08:04 kmc that's illegal 01:08:05 -!- Sgeo has joined. 01:12:50 You could probably do in an emulator since you can step each frame, to make a TAS, I suppose. However, the microphone and the initial contents of RAM are used for additional entropy if available. On the title screen (and after you win and lose), it generates (and discards) at least a thousand random numbers per frame. During the game, it generates and discards one per frame. 01:16:33 shachaf: of course, anything that makes default functionality slower will be bad for marketing your language 01:17:19 even if there's a fast RNG function, microbenchmark writers won't find it, or they'll complain about how unintuitive it is 01:17:39 whereas approximately nobody is microbenchmarking languages on the basis of 'how easy is it to write broken crypto in this language' 01:18:17 -!- nooga_ has quit (Ping timeout: 245 seconds). 01:18:49 i wonder if GHC could support lazy unboxed arrays. keep a bitmap saying whether each element is a thunk or not 01:19:35 Unboxed arrays of machine-word-sized elements? 01:19:40 it would be cool to have a language where String is some kind of awesomely efficient rope structure but still has the lazy char-at-a-time semantics 01:19:42 Sgeo: yeah, I've seen the pigeonhole principle many times. 01:19:48 shachaf: they have to be at least that big, but they could be bigger 01:20:10 Right. 01:20:38 (and of course you can hide that and just pad out things smaller than a machine word) 01:21:15 i wonder if one should put the bits at the beginning of the array, or have cache line sized chunks each with their own bitmap, or what 01:22:36 and if you had an unboxed array of Word32 on a 64-bit machine then you wouldn't need a separate bitmap at all 01:22:57 you could put the Word32 in the upper half of the machine word, and tag the low bit 01:23:42 You could do that with any Word32, not just an array... 01:23:49 kmc: I like how Haskell's "better string structure" is just an array. :( 01:23:52 putting the tags back in the etc. 01:23:58 kmc: speaking of like nonintuitiveness or whatever, I don't know if you're interested or anything but the way rdrand works is kind of interesting 01:24:50 Fiora: I have a vague understanding. it's based on drift between two oscillators, then a conditioner, then an internal PRNG? 01:25:10 they do this to avoid having analog components, which need to be redesigned on each die shrink 01:25:21 I meant, like, the UI? basically like, you use the instruction and then it sets a flag if it succeeded, otherwise you can retry 01:25:25 oh that 01:25:30 yeah interesting 01:25:31 since the bandwidth is limited (100 million calls per second or so?) across cores 01:25:35 i bet people get that wrong too 01:25:41 but yeah, the internals are really really cool 01:25:51 like, a *digital* random noise generator 01:26:09 also I think in a dream last night I wondered whether the amount of entropy in /dev/random would form an exploitable side channel in some circumstances 01:26:31 would there be a way to derive that information externally? 01:26:46 any user program can read /dev/random and see when it blocks 01:26:53 oooh. 01:26:56 which tells you about how much /dev/randoming other processes have been doing 01:27:12 `quote dream 01:27:15 150) catseye: Please wake up. Not recorded for this timezone. The big spider is not your dream \ 233) back to legal tender, that expression really makes me daydream. Like, there'd be black-market tender. Out-of-town hug shops where people exchange tenderness you've NEVER SEEN BEFORE. \ 243) Gregor, yeah, but P 01:27:23 hmmm so like 01:27:41 kmc: Linux has /proc/sys/kernel/random/entropy_avail 01:27:45 I wonder if that could be used as a timing attack, because you could use it to know when other processes are asking for entropy 01:27:51 haha nice shachaf 01:27:54 so you could use it to find out when some process is doing some particular thing? 01:27:55 Fiora: hm, yeah that too 01:28:10 but I guess if you're on the same box you could already do like a cache timing attack 01:28:44 shachaf: mine seems to clim up to 190 and then drop to 128 01:28:47 over and over 01:28:52 Yep. 01:28:54 is that because it's feeding some of that entropy into urandom? 01:29:00 I don't know. 01:29:05 It goes down to ~3 when you cat /dev/random 01:29:09 s/you/I/ 01:29:41 My entropy availability goes up to eleven. 01:29:45 it's because observing the entropy makes it less random clearly 01:30:25 The file read_wakeup_threshold contains the number of bits of entropy required for waking up processes that sleep waiting for entropy from /dev/random. The default is 64. The file write_wakeup_threshold con‐ tains the number of bits of entropy below which we wake up processes that do a select(2) or poll(2) for write access to /dev/random. These values can be changed by writing to the files. 01:32:44 The value of entropy_avail could be used as a source of entropy. 01:33:02 ion..........................no........... 01:33:57 shachaf: YOU DON’T SAY? 01:34:41 don't say what 01:36:36 kmc: speaking of keyboards do you think you could make a keylogger based on microphone input of someone typing 01:36:44 (on a laptop) 01:36:51 yes i've heard of that 01:37:15 i mean make a flash game or something that secretly logs your passwords 01:38:29 HTML5 Microphone API 01:38:42 HTML5 Keylogging API 01:39:09 also HTML5 lets you play and record audio but it has no way to isolate audio from different origins in the acoustic surroundings of the computer! 01:41:51 They are full of dumb things 01:42:12 is CoYoneda a design pattern 01:42:56 i should make a book of design patterns which gradually turns into a maths book 01:43:23 I really think the client should be programmed not to send all keys to the webpage. Someone once at FreeGeek once wanted to use a webpage to test the keyboard, and some keys interfere; I suggested instead to use the program included in Linux for this purpose, which result in not interfering with anything! 01:44:45 (It should also report the size of the document area as the screen resolution, instead of the actual screen resolution, and if a script resizes a window to a specific size, to make it larger than that so that the document area will be of the specified size instead.) 01:45:34 zzo38: you should make a twitter account 01:45:53 I don't want to make a Twitter account; I have no need for such a thing. 01:46:01 i should make a book of design patterns which gradually turns into a snake 01:46:18 No one has a *need* for it. 01:46:46 I can just use IRC or whatever. 01:47:00 How can I follow you on IRC? 01:47:23 Use the IRC log file, is one way. 02:12:15 http://www.thinkgeek.com/stuff/41/snuznluz.shtml 02:13:12 o.O it's an April Fools joke 02:13:51 https://www.beeminder.com is sort of the same thing. 02:15:21 Laughing while describing your service does not seem like the best idea ever 02:15:43 hi 02:15:48 what if your service is jokeserver 02:31:21 -!- conehead has quit (Quit: Computer has gone to sleep.). 02:43:33 -!- Phantom_Hoover has quit (Ping timeout: 268 seconds). 02:45:41 `slist 02:45:42 slist: Taneb atriq Ngevd Fiora nortti Sgeo ThatOtherPerson alot 02:45:48 Sgeo...............olist........... 02:46:07 shachaf, I can do an `olist but it would be a lie 02:46:07 you're updating the wrong comic 02:46:12 don't lie 03:03:03 -!- Frooxius has quit (Ping timeout: 245 seconds). 03:08:54 -!- elliott has quit (Quit: Changing server). 03:11:36 -!- elliott_ has joined. 03:12:00 -!- elliott_ has changed nick to Guest73516. 03:13:02 -!- Guest73516 has quit (Client Quit). 03:13:36 -!- elliott__ has joined. 03:14:26 -!- elliott__ has changed nick to elliott. 03:20:22 @karma-all 03:20:22 blah 31337 03:20:22 nobody 2000 03:20:22 c/c 499 03:20:22 ( 205 03:20:22 + 147 03:20:24 g 141 03:20:26 libc 56 03:20:28 dmwit 55 03:20:30 shachaf 53 03:20:32 monochrom 52 03:20:34 ##c 48 03:20:36 Notepad 46 03:20:38 Plugin `karma' failed with: <> 03:23:38 -!- Frooxius has joined. 03:32:41 fizzie: the freenode servers list lies about IPv6. :( 03:45:28 shachaf, `erfdate 03:46:42 Sgeo: ? 03:47:03 shachaf, Erfworld updated 03:47:10 And? 03:47:33 It amuses me that another thing updated that isn't the thing you want to see updated 03:47:42 -!- conehead has joined. 03:48:12 Note that I didn't say that I'm amused that the thing you want to update didn't update 03:49:23 Duly noted and recorded in your file for future reference. 03:54:18 your permanent record 03:54:44 kmc: that's going a little far isn't it 03:54:50 i mean it's permanent 04:07:17 -!- oerjan has joined. 04:09:58 `? indexed monad 04:10:00 Indexed monads are just categories enriched over the monoidal category of endofunctors. \ Indexed monads are just monads on an indexed category 04:10:09 * oerjan swats shachaf -----### 04:10:19 oerjan: What? 04:10:22 Oh, right. 04:10:40 `run sed -i '2s/$/./' wisdom/indexed\ monad 04:10:44 No output. 04:10:45 `? indexed monad 04:10:47 Indexed monads are just categories enriched over the monoidal category of endofunctors. \ Indexed monads are just monads on an indexed category. 04:10:52 Better. 04:11:00 * oerjan swats shachaf -----### 04:11:06 help 04:11:18 http://i.imgur.com/35Qxgty.gif 04:11:21 "considered harmful when preceded by its quotation" considered harmful when preceded by its quotation 04:11:23 is that _really_ supposed to be two different lines. 04:11:37 copumpkin: what. why. 04:11:37 kmc++ 04:11:39 http://d24w6bsrhbeh9d.cloudfront.net/photo/aXb0Bd6_460sa.gif 04:11:51 owls! 04:12:08 oerjan: Yes? 04:12:18 oerjan: There are two different meanings for the phrase. How should I do it? 04:12:37 ...i dunno. 04:13:02 why aren't any of the links loading... 04:13:13 because you're still using IE, hth 04:13:33 i think it fails at an earlier point than that hth 04:15:22 :) 04:15:38 is she eating a kitten help 04:16:07 i am 04:18:46 mmm 04:18:47 kittens 04:19:48 the other white meat? 04:21:46 -!- mnoqy has joined. 04:24:17 'malicious' is not really the standard <-- i've heard "stupid" is sometimes a good substitute hth 04:35:45 @tell taneb aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa[...] <-- you seem stressed you should relax some hth 04:35:45 Consider it noted. 04:36:01 @messages 04:36:01 You don't have any messages 04:36:06 oh misread 04:36:34 the nicks are just so similar 04:37:17 oerjan: wasn't it "incompetent' hth 04:40:47 shachaf: nope that's a later mangling hth 04:41:11 oerjan: have you ever considered quitting "hth" 04:41:45 oerjan: btw op me hth 04:41:51 oerjan: i agree, op elliott 04:42:01 then kick Phantom_Hoover and crown mnoqy 04:42:36 or wait it's been attributed to napoleon hm 04:43:00 of course he obviously said it in french hth 04:43:47 mnoqy is chaotic right 04:45:33 "Le mot impossible n'est pas français." 04:46:42 `olist 894 04:46:43 olist 894: shachaf oerjan Sgeo FireFly 04:49:26 oo 04:52:39 ts 04:55:11 hth 04:58:31 -!- Bike has joined. 05:04:53 Bike: should i sleep 05:06:02 -!- kappabot has joined. 05:06:07 no hth 05:06:49 kappabot: fuck 05:13:41 -!- kappabot has quit (Quit: Bike-is-being-unpleasant). 05:17:06 -!- sprocklem has joined. 05:20:53 kmc: what is the difference between lovers and 3-colorings of graphs.................. 05:21:06 baby don't hurt me 05:21:16 drummers have no soul in general hth 05:31:19 -!- oklopol has joined. 05:40:31 wikiquote seems to doubt the napoleon attribution, given that it is from 2003. 05:41:51 i wonder whether in a generation we will be able to distinguish false and true references at all 05:44:04 shachaf: wtf @ question 05:44:38 I hope predicative datives come up 05:44:49 `wtf predicative datives 05:44:51 why predicative datives is like wtf 05:45:43 HackEgo: *Are 05:45:46 *are 05:46:25 no its is 05:47:43 mnoqy: whoa dude are linear transformations like concatenative languages <-- you may be confused by the fact they're both monoids hth 05:48:01 or maybe categories 05:48:11 elliott: *it's 05:48:22 oerjan: *its 05:48:24 its its 05:49:08 i like how a freenode oper accidentally klined the entirety of webchat 05:49:12 by messing up the syntax 05:49:21 :') 05:49:25 and now a billion people are joining #freenode asking why they got klined 05:50:06 awesome 05:50:12 that is beautiful 05:51:03 also #freenode is literally the worst channel 05:51:10 worse than #esoteric ??? 05:51:30 why don't file: pages have a proper history link, i wanted to see if the description has been changed 05:51:56 also the kline messages say it was for "harrassing people" 05:52:01 so ppl are kind of upset about it 05:52:05 *message said 05:52:10 oh i can get to it by pressing edit on the description first 05:52:27 oerjan: hm on esolang? 05:52:53 elliott: no on wikipedia. 05:52:58 oerjan: perhaps the file is on commons 05:53:00 anyway i found it https://commons.wikimedia.org/w/index.php?title=File:Grand_Junction_from_Mass_Ave.JPG&diff=98335089&oldid=76213178 05:53:14 (edited yesterday) 05:53:19 scroll down :P 05:56:25 gah that commons stuff is confusing 05:56:57 something else that irritates me is when people link to commons pictures directly without context 05:59:05 DdEe4Aai? did kmc accidentally switch username and password? 05:59:59 that's me 06:00:11 why would my wikipedia username be related to anything else 06:00:17 it's random 06:00:19 password is random as well 06:01:08 concurrent haskell, multiocular o and methylamine... yeah that's kmc all right. 06:01:26 itt kmc has just scrambled to fix his password away from kmc 06:02:18 haha 06:02:28 you know my interests 06:02:34 they reverted my methylamine edit 06:02:36 bastards 06:02:42 oh 06:02:44 i also tried to create Category:Toroidal foods 06:02:48 deleted 06:02:51 bastards 06:03:19 why would anyone delete that!! 06:04:42 because they hate freedom 06:05:51 No, it is because they hate toriodal foods. 06:06:16 america is about freedom, the freedom to eat foods of any topological genus you like 06:06:22 and to deep fry them as well 06:06:58 kmc: technically "concurrent haskell" + "multiocular o" narrows it down to someone in this channel, and "methylamine" does the rest hth 06:07:41 what foods have genus, say, three 06:07:41 kmc: what about your reddit username 06:07:44 deep fried bagels, check 06:07:47 once upon a time i knew what it was "but i forgot" 06:08:21 i think i'm more obsessed with multiocular o than most 06:08:42 Bike: http://en.wikipedia.org/wiki/Genus_(mathematics)#Orientable_surface hth 06:08:45 Bike: well there are braided breads 06:08:53 the holes usually go away in baking I guess 06:09:44 oerjan: ?? those aren't foods! 06:09:53 although technically it's only the surface that is toroidal for bakery 06:11:39 Bike: http://en.wikipedia.org/wiki/Kringle hth 06:12:01 oh nice 06:12:09 What happened to all of kmc's edits? 06:12:26 I only see two in -- oh, never mind. 06:13:12 shachaf: they were reverted by the CIA, NSA, FBI and RIAA hth 06:13:31 sometimes with edit wars between the organizations 06:14:11 whew someone deleted the popular culture reference of methylamine 06:14:14 wtf do they use a picture of a german pretzel 06:14:19 popular culture sections are the worst thing 06:14:42 popular culture sections in popular culture: not very popular 06:15:06 (→‎Popular culture: methylamine is not capable of being aware - removed the section because it is just trivia anyway) (undo) 06:15:09 wow 06:15:24 i bet that person kills intelligent calcium, too 06:17:28 damn now i'm hungry for a pretzel 06:22:55 -!- FreeFull has quit. 06:24:53 I am not the only one who want a three button mouse with no scroll wheel. 06:26:54 -!- oerjan_ has joined. 06:27:55 -!- oerjan has quit (Remote host closed the connection). 06:28:35 zzo38: Last time you asked, I looked it up and it seemed possible to order it online. 06:37:37 oh boy a serial mouse 06:40:20 cereal mouse 06:42:38 hey remember the house with the x in the middle that people used to draw 06:42:57 good house. 06:43:31 gꙬ d house 06:44:15 shachaf: no, also what 06:45:04 ? 06:45:37 i do not remember this house 06:45:38 you draw a house as a square with diagonals with a triangle on top 06:45:52 the game is doing it without drawing a line twice 06:45:56 oh 06:46:14 so you have to start at a vertex of odd degree? 06:46:30 yeah it's babby's first eulerian whatever 06:46:37 did taht shit back in elementary school man 06:46:59 yes 06:47:12 * Bike Math Expert 06:47:14 by people i mean first-graders (i was once among their ranks) 06:47:19 o 06:47:19 / \ 06:47:19 / \ 06:47:19 o---o 06:47:19 |\ /| 06:47:21 | X | 06:47:24 |/ \| 06:47:26 o---o 06:47:29 like that 06:47:31 you never did that??????? 06:47:35 i did it 06:47:37 kmc's deprived 06:47:38 oh 06:47:43 just forgot 06:47:47 how the hell is that so common i wonder 06:48:08 did you ever join the pen 15 club 06:48:10 did you have the game where you press 1 + 1 = = = = = = = ... in a calculator 06:48:17 and see how high you could get 06:48:19 what would that do 06:48:25 add 1 repeatedly 06:48:27 missed out on pen 15 06:48:29 oh it repeats the last action 06:48:30 (or did you just do the second part (drugz joke)) 06:48:35 why not 2 * 2 = = = = = = 06:48:40 much faster 06:48:42 because the point is inefficiency hth 06:48:45 sounds cheap 06:48:45 dnh 06:48:50 why not just type 99999999 06:49:00 why not just type BB(3) 06:49:02 why not just drop out of school and go fuck yourself 06:49:11 is that a drugz joke 06:49:13 no 06:49:15 darn 06:49:17 it's a go fuck yourself joke 06:49:18 OH that reminds me 06:49:20 no that's just kmc 06:49:27 also this was all in hebrew btw hth 06:49:34 at college orientation the coordinator had to clarify by "cigarette" she meant nicotine 06:49:36 not that that matters, except for your club 06:49:44 glorious blazeit future 06:49:47