00:00:09 -!- oerjan has quit (Quit: Good night). 00:14:16 I'm not sure if Clojure's community is a good thing or a bad thing 00:14:25 On the one hand, lots of libraries, many of them good 00:14:30 On the other hand, so many idiots 00:15:05 zzo38: put a weak pull-up resistor on the bus, and require that any connected device drives the bus low when idle 00:24:47 -!- jaboja has quit (Quit: KVIrc 4.0.4 Insomnia http://www.kvirc.net/). 00:34:56 -!- DHeadshot has joined. 00:56:53 -!- Arc_Koen has joined. 00:58:14 hi 01:06:10 kmc: OK, well, I suppose it could be used on one pin to specify whether or not a program can be loaded from the device. 01:09:33 -!- JaBoJa has joined. 01:13:18 yeah, if you have a dedicated pin then the cartridge can just short that pin to ground 01:14:13 Just do a standard protocol like USB 01:19:14 It isn't USB. It is a memory address/data bus, and a few other things such as clock, audio, and some general purpose I/O. 01:25:36 -!- Nisstyre-laptop has quit (Quit: Leaving). 01:37:51 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 01:41:32 I'm having a bit of a doubt 01:42:47 Turing machines do not have a finite number of possible states, right? 01:43:19 otherwise all programs would be known to halt because they would necessarily either stop or be periodic 01:43:39 uh, I mean, they wouldn't necessarily halt but the halting problem would be solved 01:43:54 the "head" of the machine has a finite set of states 01:44:03 but the tape can grow without bound 01:44:07 yep 01:44:27 so a language which doesn't have this infinity possibility, that's what we call a finite-state automaton? 01:44:56 there are non-infinite machines other than finite state automata 01:45:10 for example, the pushdown automaton is intermediate in power between a finite state machine and a turing machine 01:45:10 oh, ok 01:45:28 also be careful, the word "language" in computability theory does not mean the same as "programming language" 01:45:36 in computability a language is just a set of strings 01:45:45 we don't assign meaning to the strings; we just ask whether they're in the set or not 01:46:54 right 01:47:05 so "programming language" you call "machine"? 01:47:17 maybe 01:47:20 I mean intuitively I'd say the "machine" is a particular program 01:47:25 yeah 01:47:35 so the programming language would be "the set of all machines" 01:47:39 languages are types of machines, then 01:47:44 yes 01:47:46 but for turing machines there is a universal machine 01:48:01 any turing machine can be emulated by passing some initial state to the universal machine 01:48:07 -!- Nisstyre-laptop has joined. 01:48:16 right 01:48:40 and of course "initial state" can be seen as an input, so basically a unversal turing machine is an interpreter? 01:48:44 yeah 01:49:13 when you're viewing turing machines as functions, the input is the initial state of the tape 01:50:07 ok 01:50:23 so I looked up what exactly a push-down automaton was - it's just a turing machine hooked to a stack 01:50:31 except with a finite tape 01:50:36 but the stack can be infinite 01:51:12 yet that's not enough to be as powerful as a turing machine? 01:53:14 no, it's not a turing machine hooked up to a stack 01:53:20 it's a finite state machine hooked up to a stack 01:53:36 fsm: (state, input character) -> state 01:54:15 pda: (state, input character, top of stack) -> (state, thing to push or not) 01:54:25 Is it logically determined for every UTM program if it halts or not? Or does there exist programs with stop problem unsolvable like continuum problem. 01:54:47 turing machine: (state, character under head) -> (state, new character under head, direction to move on tape) 01:55:35 a turing machine with finite tape is equivalent to a finite automaton 01:56:04 just like a turing machine with n independent state variables is equivalent to a turing machine with one state variable 01:56:30 right 01:56:35 the only requirement is that the set of states is finite 01:56:51 but the input character can be taken from an infinite alphabet? 01:56:52 so you can use finite-length tuples over finite sets of states 01:56:53 no 01:57:07 so input is bounded 01:57:35 yeah 01:57:47 -!- NihilistDandy has quit (Quit: ["Textual IRC Client: www.textualapp.com"]). 01:58:38 @where sneaky 01:58:38 dropFromEnd n xs = zipWith const xs (drop n xs) 01:58:47 ☝ best function 02:00:46 Arc_Koen: there is a wrinkle in what i said though 02:01:02 a deterministic finite state machine is defined by a function (state, input character) -> state 02:01:31 but a nondeterministic finite state machine has a set of "possible" new states 02:01:41 yup 02:01:53 it turns out that, if some language is recognized by a NFA, you can make a DFA to recognize it 02:01:56 (and vice versa) 02:01:59 but this is not true for pushdown automata 02:02:09 nondeterministic pushdown automata are strictly more powerful than deterministic ones 02:02:31 but it is true for turing machines 02:02:43 that's what the wikipedia page said, but they explained why in one sentence and it was grammatically incorrect and not really helping 02:02:54 (until you start talking about the execution time rather than just what's possible or impossible) 02:03:09 which thing did wikipedia try to explain? 02:03:29 why you couldn't turn a nondeterministic pushdown automaton into a deterministic one 02:03:43 yeah, i don't remember offhand 02:04:04 Unlike finite-state machines, there exists no general alogorithm of turning a NDPDA into an equivalent DPDA, because that the problem of determining whether a http://en.wikipedia.org/wiki/Context-free_language is deterministic is decidable, which is not.[1] 02:04:26 (please excuse the weird way my irc client copies links) 02:07:47 finding a proof of this is surprisigly hard 02:07:50 or maybe i just suck at googling it 02:07:52 http://cstheory.stackexchange.com/questions/9673/why-is-non-determinism-push-down-automata-necessary 02:13:04 so in their example they say you have a word as input 02:13:25 you said you had only a character - if the word's length is not bounded, then it's not the same, is it? 02:24:08 -!- JaBoJa has quit (Quit: Bye). 02:27:44 a finite state machine or pushdown automaton processes one character at a time 02:28:15 the input is a word of finite length, but it can be any finite length, there is no bound to how big the word could be 02:28:22 (of course you can make a machine which rejects all words bigger than n) 02:28:41 hmmm but does it have to process the next character at every tick? 02:28:52 a deterministic automaton yes 02:29:40 in some presentations, a nondeterministic automaton can have "ε transitions" which move from one state to another without consuming a character 02:29:51 but this is a just notational convenience 02:30:27 because you could just add everything reachable from ε transitions to the set of possible next states 02:30:56 a good book on this stuff is _Introduction to the Theory of Computation_ by Sipser 02:31:16 it presents everything in order using consistent notation etc 02:31:30 much nicer than reading a bunch of wikipedia pages 02:31:44 haha 02:31:57 yep I definitely should read books 02:34:47 hmmmm 02:35:03 but still, if there are an infinity of possible words 02:35:51 oh, right, you said the epsilon thing was only for nondeterministic automatons 02:38:01 actually i'm not sure the ε transitions can be removed from a NPDA 02:38:16 you can use them to push or pop more than one stack character per input character 02:38:56 on a dpa with a finite number of states I'm pretty convinced it cannot be removed 02:39:12 the set of states is always finite 02:39:19 right 02:39:35 i mean it's not impossible to talk about infinite number of states 02:39:40 but it's not what people usually talk about 02:39:44 so where exactly does the "finite-state automaton" name come from? 02:39:58 there are a finite number of states 02:40:06 i.e. a finite amount of state 02:41:38 ok so that "finite" means it really is finite, opposite to a turing machine which tape can be in an infinite amount of states 02:42:16 yeah 02:42:51 a pushdown automaton also has an infinite number of states icluding the stack 02:43:26 (when i said "the set of states is always finite" i meant the states not including the stack, i.e. the things typically drawn as nodes in a graph 02:43:29 ) 02:43:33 I'm thinking they should have bothered to find a different word for the "states" in the automaton and the total "states" the machine can be in 02:43:39 yeah exactly 02:48:23 If you lose a game of Double Fanucci against a dragon, you will die, isn't it? However, I lost against a half-dragon, so I only lost five perica instead. 02:49:37 a half-dragon? I thought we called them lizards 02:51:09 This is different half dragon though. 02:51:23 besides, i'm guessing half-dragons are less powerful than whole dragons, so losing against a half-dragon should be more severely punished 02:52:47 (as in, losing against a half-dragon implies you would have lost against a whole dragon as well) 02:53:38 I don't think it would imply; it depend how the cards are dealt. 02:54:44 As well as on how good you are at the game. 02:55:37 well except if it's a game of chance, and you're considering that the winner will bully the loser, in which case yeah I guess being bullied by a whole dragon is more scary 02:56:24 wait, are you playing Zork? 02:56:26 It is a card game, so there would be chance involved, but skill is also involved 02:56:48 No, it is not Zork. It is what I wrote in my character background story for Dungeons&Dragons. 02:57:19 zzo38: i have been thinking that some of those x-bit sports you have been playing could be played without a computer by a few people around a table 02:57:34 but i dont want to interrupt right now 02:58:26 itidus21: Play by cards? 02:59:01 like the boxing and the basketball 02:59:55 i was thinking more of having a GM 03:00:34 (zzo38: my point was that, if you're playing, say, a go tournament (or chess tournament, or any other game) and every game you play affects your ranking, then loosing against a "strong" opponent will make you loose less ranking points than losing against a "weak" player) 03:00:41 Sure you could, but I would think it would be better by cards 03:01:27 Arc_Koen: OK. But how good you are at these kind of games (chess, cards, go, whatever) is not your physical strength. 03:01:30 I'm tempted to just stick with Eclipse 03:01:46 zzo38: well, a box tournament then 03:01:52 OK 03:03:12 though yeah, if you can be physically "damaged" during the game then playing against someone too strong might be dangerous - though if the damage is already implied by the fact that you have lost, it could not make a difference 03:04:06 is this like playing chess against a wookie? 03:04:39 also, the way you said "play by cards" just gave me the idea that any card game which doesn't include a pile, but rather have the cards dealt among the players at the beginning, could be played by email 03:05:01 like, you send the card you want to play along with the letter 03:05:01 well not chess.. i don't know what the actual game is called 03:05:21 Arc_Koen: OK, if you prefer that way. 03:05:33 ^Dejarik 03:05:42 itidus21: against a wookie, I think it's less dangerous to loose than to win (in case the wookie is a sore looser) 03:05:51 -!- Jafet has joined. 03:07:31 i see, a dragon is not like a wookie 03:12:51 less hair, more scales 03:15:16 oh I had an idea for a nondeterministic language today 03:15:31 basically it would be a monopoly-like board game 03:15:56 where all the players are controlled by the computer, with dice being rolled 03:16:20 and the cells on the board, or the cards to be drawn, would affect the memory and trigger some computations 03:20:12 -!- Jafet has quit (Quit: Leaving.). 03:51:16 -!- TeruFSX_ has joined. 04:04:36 -!- dajfsa has joined. 04:04:39 erfjoirgejroijg 04:04:42 werjero 04:04:56 oioieoiroeiro 04:10:42 `welcome dajfsa 04:10:51 dajfsa: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 04:16:46 hi 04:19:17 q 04:19:18 qqq 04:19:21 q qq q q qq 04:19:22 itidus21: q? 04:19:26 !@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@! 04:19:29 /////////////// 04:21:59 qqqq 04:22:17 q qq q q qq q q q qq 04:26:45 :wq 04:27:27 > (intercalate " " . map (flip (replicate 'q'))) [1..] 04:27:28 Couldn't match expected type `GHC.Types.Int' 04:27:28 against inferred type ... 04:27:35 duh 04:27:38 > (intercalate " " . map (flip replicate 'q')) [1..] 04:27:40 "q qq qqq qqqq qqqqq qqqqqq qqqqqqq qqqqqqqq qqqqqqqqq qqqqqqqqqq qqqqqqqqq... 04:28:06 * ion remembers unwords 04:35:57 machine code uses goto? when writing functional programs it's better to have recursive calls be the last thing in a function... I wonder if, on a computer where machine code would use comefroms instead of gotos, it would be better to have recursive calls be the first thing in a function 04:37:24 (that thought was sponsored by the It Is 6 am And I Havent Slept Yet industry) 04:39:50 head llac optimization 04:40:50 has there been much work on esoteric quantum programming languages 04:41:42 there is quantum brainfuck at least 04:41:44 of course 05:10:49 -!- zzo38 has quit (Read error: Connection reset by peer). 05:11:55 -!- zzo38 has joined. 05:18:47 -!- Nisstyre-laptop has quit (Read error: Connection reset by peer). 05:21:05 -!- Nisstyre-laptop has joined. 05:52:09 well my interrogations about turing-completeness and input/output were legitimate I think 05:52:49 consider a language which has a function "print" and a function "read" which allow to output and input some stuff 05:53:10 and it also has other functions, and considering those other functions only you manage to prove it turing-complete 05:53:49 then someone asks you to write a program in that language that takes an input n, and outputs fib(n) 05:53:49 Errr 05:54:04 well it may not be possible 05:54:33 And? Claiming that a language is TC does not claim that it is possible to do that. 05:55:44 well, I thought turing-completeness was a way to describe what algorithms the language could implement 05:56:20 and there you have a language you said was tc and yet it cannot do something as simple as giving you fib(n) 05:56:29 It is. Input is not usually considered to be part of algorithms, and even if it is, it's certainly outside the scope of Turing-completeness. 05:56:36 It can give you fib(n) 05:56:46 The question of how you get “n” is different. 05:57:08 how can it give me fib(n)? 05:57:19 it can ran computations, but it has no ways of giving me a result 05:57:32 It doesn't have to. 05:57:38 So long as it's calculated that result, it's done. 05:57:44 that's where I disagree 05:57:53 Your disagreement is irrelevant, you're simply wrong. 05:58:07 whoa that's really interesting talking with you 05:58:20 I have to go sleep anyway, have a nice day 05:58:41 -!- Arc_Koen has quit (Quit: that's dr. turing to you, punk). 05:59:01 *shrugs* 06:22:11 -!- ztirf has joined. 06:22:18 -!- ztirf has quit (Client Quit). 06:35:03 -!- copumpkin has quit (Ping timeout: 268 seconds). 06:36:13 -!- copumpkin has joined. 06:48:17 -!- atriq has joined. 07:06:16 -!- xroslight has joined. 07:06:30 我能吞下粘土而不伤身体 07:08:29 How much of a memory hog is Eclipse, exactly? 07:09:01 不知道 07:15:44 -!- ion has quit (Ping timeout: 252 seconds). 07:16:53 这里都是中国人吗? 07:19:03 -!- oerjan has joined. 07:20:09 -!- TeruFSX has quit (Ping timeout: 256 seconds). 07:23:21 -!- oerjan has quit (Client Quit). 07:41:25 `welcome guy_who_maybe_should_speak_English 07:41:36 guy_who_maybe_should_speak_English: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 07:42:06 thizzie 07:43:47 Floozie. 07:43:53 @wn floozie 07:43:53 *** "floozie" wn "WordNet (r) 3.0 (2006)" 07:43:54 floozie 07:43:54 n 1: a prostitute who attracts customers by walking the streets 07:43:54 [syn: {streetwalker}, {street girl}, {hooker}, {hustler}, 07:43:54 {floozy}, {floozie}, {slattern}] 07:43:57 Maybe not that. 07:44:10 i watched this is spinal tap today. it occured to me at some point that the main motivation for programming to be performance art is so that programmer fashion can happen 07:45:29 -!- oerjan has joined. 08:03:44 -!- xroslight has left. 08:17:01 -!- Nisstyre-laptop has quit (Remote host closed the connection). 08:17:14 -!- copumpkin has quit (Ping timeout: 240 seconds). 08:17:49 -!- copumpkin has joined. 08:25:51 -!- zzo38 has quit (Remote host closed the connection). 08:46:20 -!- Taneb has joined. 08:46:49 -!- atriq has quit (Ping timeout: 260 seconds). 08:53:45 -!- nooga has joined. 09:11:36 -!- KingOfKarlsruhe has joined. 09:17:05 -!- monqy has quit (Quit: hello). 09:33:55 -!- Phantom_Hoover has joined. 10:53:27 -!- yiyus has quit (Ping timeout: 268 seconds). 10:53:50 -!- yiyus has joined. 10:57:15 -!- fungot has quit (Ping timeout: 250 seconds). 11:03:50 -!- JaBoJa| has joined. 11:04:38 -!- JaBoJa| has changed nick to jaboja. 11:34:43 -!- FireFly has quit (Ping timeout: 245 seconds). 11:35:07 -!- ais523 has joined. 11:44:16 -!- FireFly has joined. 11:51:09 -!- zzo38 has joined. 12:11:23 -!- MoALTz has joined. 12:22:29 -!- KingOfKarlsruhe has quit (Quit: ChatZilla 0.9.89 [Firefox 15.0.1/20120905151427]). 12:24:40 -!- oerjan has quit (Quit: Now the Jolverine loops work again). 12:35:23 -!- FireFly has quit (Changing host). 12:35:23 -!- FireFly has joined. 12:41:59 OK, so if you're looking for a (reasonably sensible) syntax for something that can be a list or tuple or both, what should it be? 12:47:17 rojoerj 12:47:24 ,, ,, , , , 12:47:28 ais523: ? | ( | ) ? ? 12:47:33 ``` 12:47:39 ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: ``: not found 12:48:31 :Q 13:04:51 -!- xiaoding has joined. 13:04:56 -!- xiaoding has left. 13:07:03 ais523: how about {x,y} 13:07:04 ais523: or [x,y] 13:07:05 ais523: or (x,y) 13:07:15 former is probably my favourite although {} are often overloaded for other purposes 13:07:20 is also an option 13:07:26 [x,y] i find ugly for tuples, (x,y) i find ugly for lists 13:07:38 ais523: however i would question what your distinction between list and tupl eis 13:07:45 & if such an overloaded literal actually makes sense given that 13:08:01 qqqqQQqqqQ*$(@(##(@#*(@#*(@#*(@*(*(@((@~)------------oooooooooooooooooooooooooo===>>>>>>$>$>$>$>$ 13:09:03 nice rant by arc_koen in the logs 13:10:59 zzo38: what is the internet 13:12:55 dajfsa: Internet is the TCP/IP computer network connected by everything. 13:15:49 +x,y- 13:18:27 -!- atriq has joined. 13:20:07 @messages? 13:20:07 Sorry, no messages today. 13:20:10 Yay! 13:26:34 -!- kinoSi has quit (Read error: Connection reset by peer). 13:27:01 -!- kinoSi has joined. 13:29:14 lol. many things in the logs! 13:29:55 Such as? 13:34:45 -!- Taneb has quit (Ping timeout: 248 seconds). 13:35:58 The Wikipedia article for call/cc describes to access the continuation from outside of call/cc, and I think I have made that work with Haskell too by making up a newtype of it. 13:36:21 zzo38, isn't that in Control.Monad.Cont? 13:37:37 atriq: There is Cont and ContT in there, but I mean I could make something like this: newtype C r x = C (C r x -> Cont r x); which I think would be the correct type to return the current continuation from callCC. 13:37:57 Hmm 13:38:07 I still haven't understood call/cc 13:38:45 Read the Wikipedia it describe. The esolang wiki article for Unlambda also links to some related information. 13:38:55 atriq: such as whales! 13:38:59 `log whale 13:39:34 No output. 13:39:39 `log whale 13:39:53 2011-07-23.txt:00:17:06: very like a whale 13:40:04 `log wales 13:40:16 2010-12-26.txt:05:18:39: rms doesn't quite give the same air as jimbo wales 13:40:29 `log wails 13:40:36 2012-09-22.txt:13:40:29: `log wails 13:40:49 `log [w]ails 13:40:56 2012-09-22.txt:13:40:29: `log wails 13:41:00 `log [w]ails 13:41:07 2012-09-22.txt:13:40:56: 2012-09-22.txt:13:40:29: `log wails 13:41:13 fine 13:41:31 `log [w]ells 13:41:39 2007-11-30.txt:20:08:20: Giving the old ones energy would make them temperature wells; creating and destroying particles would make them pressure wells. 13:41:49 `log [w]alls 13:41:57 2009-10-15.txt:13:52:21: [The walls, of which there aren't any, melt.] 13:42:05 `log [w]ills 13:42:11 2012-04-20.txt:02:44:02: you wills ee 13:42:28 In other news, I've finally installed the Haskell Platform correctly on this computer with GHC 7.* 13:48:42 Every other time I messed up installing the docs 13:50:15 -!- carado has quit (Quit: Leaving). 13:50:39 -!- carado has joined. 14:01:08 -!- ztirf has joined. 14:01:17 -!- ztirf has quit (Client Quit). 14:02:39 -!- TeruFSX has joined. 14:05:27 -!- ogrom has joined. 14:19:29 -!- TeruFSX has quit (Read error: Connection reset by peer). 14:24:33 ais523: Welcome to saturday 14:49:40 -!- atriq has quit (Remote host closed the connection). 14:51:49 -!- jaboja has quit (Ping timeout: 244 seconds). 14:58:00 -!- atriq has joined. 15:09:00 You know what? 15:09:06 I'm going to go and read a book 15:09:09 Bye 15:09:11 -!- atriq has quit (Quit: Leaving). 15:10:33 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 15:12:59 -!- JaBoJa has joined. 15:13:27 -!- ogrom has quit (Read error: Connection reset by peer). 15:15:35 -!- sivoais has quit (Quit: Lost terminal). 15:21:09 -!- ogrom has joined. 15:23:06 -!- JaBoJa has quit (Read error: Connection reset by peer). 15:24:05 -!- JaBoJa has joined. 15:24:39 -!- Phantom_Hoover has joined. 15:27:59 -!- sivoais has joined. 16:18:16 Dog dog dog dog dog dog dog dog dog 16:23:05 Cat cat cat cat cat cat cat cat cat 16:24:28 Cat dog cat dog cat dog cat dog cat 16:29:15 nice, i made a program that dies with ETOOMANYREFS 16:29:35 this errno is only produced in one place in the entire Linux kernel 16:31:56 -!- Vorpal has joined. 16:39:56 Where? 16:40:15 #!/usr/bin/env cat 16:40:21 dog dog dog dog dog dog dog dog 16:40:31 dong dong dong dong dong dong dong dong 16:40:55 fish fish fish fish fish fish fish fish fish 16:41:10 Buffalo buffalo Buffalo buffalo buffalo buffalo Buffalo buffalo. 16:41:42 Triadobatrachus triadobatrachus triadobatrachus triadobatrachus triadobatrachus triadobatrachus triadobatrachus triadobatrachus triadobatrachus 16:49:06 -!- uroboroo has joined. 16:50:37 -!- uroboroo has left ("PING 1348332637"). 16:58:21 -!- Lumpio- has changed nick to LumpioI. 16:59:33 -!- itidus20 has joined. 16:59:53 -!- zzo38 has quit (Remote host closed the connection). 17:02:49 -!- itidus21 has quit (Ping timeout: 246 seconds). 17:19:45 -!- Nisstyre-laptop has joined. 17:21:32 -!- atriq has joined. 17:23:05 Well, that was fun 17:26:54 -!- ion has joined. 17:30:27 -!- JaBoJa has quit (Read error: Connection reset by peer). 17:31:14 -!- JaBoJa has joined. 17:50:21 -!- Lumpio- has joined. 18:17:21 -!- JaBoJa has quit (Read error: Connection reset by peer). 18:17:45 atriq: Q q q 18:17:56 Q q r 18:17:59 -!- JaBoJa has joined. 18:19:10 -!- JaBoJa has quit (Read error: Connection reset by peer). 18:19:41 -!- JaBoJa has joined. 18:20:33 -!- LumpioI has quit (Quit: no more irssi). 18:22:22 -!- JaBoJa has quit (Read error: Connection reset by peer). 18:23:39 -!- JaBoJa has joined. 18:28:15 -!- copumpkin has quit (Ping timeout: 256 seconds). 18:28:50 -!- copumpkin has joined. 18:33:51 -!- oerjan has joined. 19:01:10 -!- JaBoJa has quit (Read error: Connection reset by peer). 19:02:12 -!- JaBoJa has joined. 19:03:14 -!- JaBoJa has quit (Read error: Connection reset by peer). 19:06:01 Deth 19:06:17 -!- dajfsa has quit (Quit: Lost terminal). 19:06:33 well that was the end of him, then. 19:11:55 -!- oerjan has quit (Quit: leaving). 19:12:04 -!- oerjan has joined. 19:20:19 -!- monqy has joined. 19:28:34 -!- TeruFSX_ has quit (Ping timeout: 240 seconds). 19:35:01 -!- Sgeo has quit (Read error: Connection reset by peer). 19:36:51 -!- Sgeo has joined. 19:39:31 Who even is dajfsa 19:44:10 -!- Phantom_Hoover has quit (Ping timeout: 246 seconds). 19:54:59 -!- atriq has quit (Remote host closed the connection). 20:11:20 -!- monqy has quit (Quit: hello). 20:22:01 -!- Phantom_Hoover has joined. 20:57:22 -!- atriq has joined. 21:05:55 -!- ogrom has quit (Quit: Left). 21:09:43 http://www.msr-inria.inria.fr/events-news/feit-thompson-proved-in-coq 21:15:42 -!- MoALTz has quit (Ping timeout: 264 seconds). 21:17:22 kmc: wow. i think this is actually quite big. 21:18:34 kmc: roconnor was just talking about that at his talk the other day. 21:18:40 He did some of it, I think. 21:20:51 well he's listed in the sidebar of that page... 21:21:43 not directly related though 21:21:52 (afaict) 21:22:03 Galois Connections, Poset-Enriched Categorical Logic, and Type Theory 21:23:37 it seems to me that the larger the proof of a theorem, the more important it is to get it formally verified 21:23:52 although of course the more difficult, too 21:27:12 Vorpal: was it you who changed C-INTERCAL to use an actual bool type? 21:27:40 -!- copumpkin has changed nick to COPUMPKIN. 21:28:32 -!- COPUMPKIN has changed nick to copumpkin. 21:35:43 INTERNET 21:35:46 INTERNET, TELL ME 21:35:49 Should I buy an accordion? 21:36:14 Are you able to play the accordion, or are you able to get accordion lessons? 21:36:30 I am able to play the piano and various other instruments, and am not incompetent. 21:36:40 Then the answer is hell 21:36:41 Freaking 21:36:42 Yes 21:36:52 But I'm SO CHEAP. 21:37:04 Hey, it was your idea 21:37:17 Also, go to anime conventions dressed as an esolang 21:37:25 kmc: thanks for giving me my first r/math post, btw :P 21:37:44 (should totally be a thing that happens) 21:37:47 actually, first reddit post whatsoever 21:38:24 Feit-Thompson theorem has been, like, TOTALLY checked in Coq 21:38:55 My first reddit post was a Muse/Sweet Bro and Hella Jeff mashup on /r/homestuck/ that received one downvote and no comments 21:40:02 :( 21:41:46 atriq: :( 21:42:37 8 notes on Tumblr, though! 21:42:53 btw, I like Debian's condensed version of INTERCAL's development history: http://bugs.debian.org/cgi-bin/version.cgi?info=1;collapse=1;found=0.29-2;package=intercal 21:43:01 When me posting a screenshot of a tweet got 12... 21:43:44 hahaha 21:44:33 kmc: I watched some episodes of that television series. 21:44:39 which one? 21:44:50 Poset-Enriched Categorical Logic: The Television Series? 21:45:14 _Breaking Bad_ 21:45:23 ah 21:45:31 are you watching it from the beginning? 21:45:42 The ones I watched were the first ones. 21:48:15 -!- variable has changed nick to constant. 21:59:45 -!- nooga has quit (Read error: Connection reset by peer). 22:03:06 -!- nooga has joined. 22:04:23 I think I've just blown someone's mind by playing along with someone else's joke 22:05:13 how evil. 22:05:37 We've convinced her that Power Rangers was originally a British series 22:05:40 And that it was awful 22:11:18 power rangers is actually a spinoff of dr. who 22:12:30 power doctors, doctor rangers, ranger who 22:12:39 'For example in Mighty Morphin, alien wizard Zordon recruits "teenagers with attitude" to harness the power of the dinosaurs to overcome the forces of evil space alien Rita Repulsa.' 22:12:50 you really cannot make this show sound more awful than it actually is 22:14:31 What, Dr. Who? 22:16:16 I liked Power Rangers when I was a kid. 22:16:33 Although I think I did recognize how repetitive it is 22:16:34 alien "wizard", recruits teenagers, fights evil space aliens... that's doctor who indeed 22:17:14 -!- monqy has joined. 22:18:52 monqy: hi monqy 22:19:02 hi 22:28:09 15:27 If you guys were to explain monads to a newbie, how would you do it? 22:28:28 I should probably leave now. :-( 22:33:05 Badly. 22:38:49 -!- nooga has quit (Ping timeout: 246 seconds). 22:45:22 -!- segorev has joined. 22:49:28 hhhiii 22:49:49 `welcome segorev 22:50:00 segorev: Welcome to the international hub for esoteric programming language design and deployment! For more information, check out our wiki: http://esolangs.org/wiki/Main_Page. (For the other kind of esoterica, try #esoteric on irc.dal.net.) 22:50:53 hi 22:51:00 ) 22:51:29 We also talk about: maths, Haskell, Homestuck, Dwarf Fortress, Finland, television, Gregor's taste in clothes and accessories... 22:51:41 i know) 22:51:45 Hexham 22:51:55 Is Hexham a kind of Finland? 22:52:09 My taste in clothes is AMAZING, TYVM. 22:52:21 Hexham's a kind of Dwarf Fortress 22:52:33 -!- benuphoenix has joined. 22:52:35 Is television a kind of maths? 22:52:39 I don't even own one. 22:52:42 Who knows? 22:53:26 can you own kinds of maths? 22:53:28 Television /involves/ math :) 22:53:47 Television? TV?) 22:53:57 You wouldn't steal a kind of maths! 22:54:17 Television and math? Is this stuff compatible? 22:55:02 question: if a system wih 12GB of ram costs $1000 and the same system with 16GB costs $1200, is the sstem with more ram worth it? 22:55:23 tggggggggghtjuuy0v= 22:55:30 oops 22:55:33 How much would it cost to buy the additional RAM separately? 22:55:43 not sure 22:56:06 but imd need the unit beforehand 22:56:07 Is that ECC RAM or something? Because normal DDR3 RAM is *much* cheaper than that. 22:57:06 tggggggggghtjuuy0v= <-- what _is_ with the weird words people use today 22:57:35 a 4gb ddr3-1333 chip costs? 22:57:55 1333? That’s even cheaper than what i was thinking of. 22:58:24 is this system bad now that it uses 1333? 22:59:33 there's gotta be something else 23:00:07 i'm on road. i'll get back to you when i get home 23:00:08 benuphoenix: In Finland, 16.90 € http://www.verkkokauppa.com/fi/product/15419/cbdjm/Kingston-Valueram-2GB-1333MHz-DDR3-CL9-muistimoduli 23:00:16 whoops, sorry 23:00:19 I misread. 23:00:53 benuphoenix: 19.90 € http://www.verkkokauppa.com/fi/product/4110/dghjq/Kingston-HyperX-blu-4-GB-1600-MHz-DDR3-CL9-muistimoduli 23:01:19 For some reason, the 4 GiB Valueram 1333 MHz and HyperX 1600 MHz modules have the same price. 23:01:48 does byte start with a t in finnish? 23:02:29 tybä 23:03:13 gigatavua, apparently 23:04:00 they're not big on b's, come to think of it 23:05:44 do they even have it at all? 23:06:00 olsner: Even though everyone learned that you don’t “translate” international unit symbols, Microsoft™ followed by the Finnish media began changing B to t for some reason. 23:06:20 shachaf: television is mostly cardboard and drugs and only a little bit math 23:06:30 +in school 23:06:52 * shachaf read that as "only a little bit meth" 23:07:00 watch more breaking bad 23:07:06 * shachaf blamc 23:09:51 "Finnish is written with [an] alphabet that includes the distinct characters Ä and Ö, and also several characters (b, c, f, q, w, x, z and å) reserved for words of non-Finnish origin." 23:12:15 wax 23:12:42 What's a ridiculous Finnish word that everyone should know? 23:12:55 Yliesierikoisapulaisvaravaurioraivausvuorovarausratkaisupäällikkö 23:13:00 "suomi" 23:13:03 It means "silly person" 23:13:09 ion, what does that mean? 23:14:05 Google reckon's it's probably Finnish for something but has no idea what 23:14:27 you need to add spaces to help it parse out the words in the word 23:14:41 Someone on the Intertubes translated it as “chief superior pre-special assistant vice damage-clearing turn reservation solution executive” but i’m not sure that’s 100 % correct. 23:14:59 (“pre-special”, huh?) 23:15:50 but you're the finnish person here, you should know right? 23:16:01 * shachaf is Finnish! 23:16:13 shachaf: prove it 23:16:17 I know what it means in Finnish but i’m not familiar enough with title jargon in English. 23:16:35 shachaf, there's about half a dozen finns online at any one time 23:17:30 Okay, the proper translation for esi- in this case would be fore-, not pre-. 23:17:59 fore-special? 23:18:30 The fore- isn’t really attached to the following word, you’d need to change the word order as well to translate it properly. 23:18:37 I mean, the esi- 23:18:44 yliesi is like over-pre-something? 23:19:16 overformynderiet 23:19:18 Hang on 23:19:35 Isn't it about half two in the morning in Finland 23:19:38 @time ion 23:19:38 Local time for ion is Sun, 23 Sep 2012 02:19:38 +0300 23:19:51 THAT MEANS GOODNIGHT 23:19:53 -!- atriq has quit (Quit: Leaving). 23:20:11 why did he quit because it is late in finland? 23:20:33 sure, everyone knows hexham is in finland 23:20:38 Here’s a long single word. The previous one was a compound word. kumarreksituteskenteleentuvaisehkollaismaisekkuudellisenneskenteluttelemattomammuuksissansakaankopahan 23:21:10 why is that not compound? is it all suffixes and conjugations? 23:21:31 yeah 23:22:02 looks like it breaks google translate somehow, maybe they have a finnish parser that is actually trying to parse the word 23:23:03 doesn't google translate work purely statistically with no builtin language knowledge? 23:24:15 yes, afaik 23:24:51 oh well, I took the time to rate this translation "unhelpful" 23:25:50 Why does Kerbal Space Program hate me ;_; 23:29:17 Phantom_Hoover: it's probably written in a brainfuck derivative 23:29:30 i think it's written in c# 23:29:49 there should be a Gerbil Space Program 23:29:57 which is in many ways a brainfuck derivative 23:30:03 it's a little known fact 23:30:27 the greatest success of the gluing things to skateboards principle 23:30:36 thinking about it, wouldn't gerbils need practically just as big rockets to get into orbit as the human space program? 23:31:39 i thought the size of the rocket would be proportional to the mass of the payload 23:33:01 yes, but is the mass of the payload proportional to the size of humans? 23:34:35 -!- carado has quit (Quit: Leaving). 23:34:46 oh, apparently the average adult gerbil weighs about 70 g ... they're a lot more smaller than I thought 23:35:21 olsner clearly has been thinking of gerbils as fearsome human-sized monsters 23:37:47 which is better: intel h67 chipset or intel b75 chipset?\ 23:40:27 Sgeo, ion, oerjan? Continuing conversation from before... 23:43:54 * Sgeo has no idea 23:44:23 I can tell you which language I'm currently mostly interested in: Clojure. This is completely unhelpful for your question, though. 23:45:20 oh...h67 is sandy bridge and b75 is ivy bridge 23:45:31 Sgeo: Wait, you're interested in Clojure?! 23:45:32 i think i want the ivy, right? 23:47:11 (dotimes [n 500] (println "Yes, shachaf.")) 23:47:22 especially with an ivy processor 23:47:22 oerjan: yes, something like http://en.wikipedia.org/wiki/Josephoartigasia_monesi 23:47:26 benuphoenix: You want Haswell, dude. 23:47:35 shachaf, what's wrong with Clojure? 23:48:02 Sgeo: Nothin' 23:48:17 (no, actually I was just thinking approximately rabbit-sized) 23:50:11 olsner: so not like these, then? http://www.webcomicsnation.com/shaenongarrity/narbonic_plus/series.php?view=archive&chapter=14370 23:55:39 assuming the gerbils were also working on this in the '60s, they'd need about a thousand gerbils' weight in computers 23:55:48 shachaf: can't wait