00:00:09 -!- oerjan has quit (Quit: Good night).
00:14:16 <Sgeo> I'm not sure if Clojure's community is a good thing or a bad thing
00:14:25 <Sgeo> On the one hand, lots of libraries, many of them good
00:14:30 <Sgeo> On the other hand, so many idiots
00:15:05 <kmc> 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.
01:06:10 <zzo38> 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 <kmc> yeah, if you have a dedicated pin then the cartridge can just short that pin to ground
01:14:13 <Lumpio-> Just do a standard protocol like USB
01:19:14 <zzo38> 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:42:47 <Arc_Koen> Turing machines do not have a finite number of possible states, right?
01:43:19 <Arc_Koen> otherwise all programs would be known to halt because they would necessarily either stop or be periodic
01:43:39 <Arc_Koen> uh, I mean, they wouldn't necessarily halt but the halting problem would be solved
01:43:54 <kmc> the "head" of the machine has a finite set of states
01:44:03 <kmc> but the tape can grow without bound
01:44:27 <Arc_Koen> so a language which doesn't have this infinity possibility, that's what we call a finite-state automaton?
01:44:56 <kmc> there are non-infinite machines other than finite state automata
01:45:10 <kmc> for example, the pushdown automaton is intermediate in power between a finite state machine and a turing machine
01:45:28 <kmc> also be careful, the word "language" in computability theory does not mean the same as "programming language"
01:45:36 <kmc> in computability a language is just a set of strings
01:45:45 <kmc> we don't assign meaning to the strings; we just ask whether they're in the set or not
01:47:05 <Arc_Koen> so "programming language" you call "machine"?
01:47:20 <Arc_Koen> I mean intuitively I'd say the "machine" is a particular program
01:47:35 <Arc_Koen> so the programming language would be "the set of all machines"
01:47:39 <kmc> languages are types of machines, then
01:47:46 <kmc> but for turing machines there is a universal machine
01:48:01 <kmc> any turing machine can be emulated by passing some initial state to the universal machine
01:48:07 -!- Nisstyre-laptop has joined.
01:48:40 <Arc_Koen> and of course "initial state" can be seen as an input, so basically a unversal turing machine is an interpreter?
01:49:13 <kmc> when you're viewing turing machines as functions, the input is the initial state of the tape
01:50:23 <Arc_Koen> so I looked up what exactly a push-down automaton was - it's just a turing machine hooked to a stack
01:51:12 <Arc_Koen> yet that's not enough to be as powerful as a turing machine?
01:53:14 <kmc> no, it's not a turing machine hooked up to a stack
01:53:20 <kmc> it's a finite state machine hooked up to a stack
01:53:36 <kmc> fsm: (state, input character) -> state
01:54:15 <kmc> pda: (state, input character, top of stack) -> (state, thing to push or not)
01:54:25 <JaBoJa> 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 <kmc> turing machine: (state, character under head) -> (state, new character under head, direction to move on tape)
01:55:35 <kmc> a turing machine with finite tape is equivalent to a finite automaton
01:56:04 <kmc> just like a turing machine with n independent state variables is equivalent to a turing machine with one state variable
01:56:35 <kmc> the only requirement is that the set of states is finite
01:56:51 <Arc_Koen> but the input character can be taken from an infinite alphabet?
01:56:52 <kmc> so you can use finite-length tuples over finite sets of states
01:57:47 -!- NihilistDandy has quit (Quit: ["Textual IRC Client: www.textualapp.com"]).
01:58:38 <lambdabot> dropFromEnd n xs = zipWith const xs (drop n xs)
02:00:46 <kmc> Arc_Koen: there is a wrinkle in what i said though
02:01:02 <kmc> a deterministic finite state machine is defined by a function (state, input character) -> state
02:01:31 <kmc> but a nondeterministic finite state machine has a set of "possible" new states
02:01:53 <kmc> it turns out that, if some language is recognized by a NFA, you can make a DFA to recognize it
02:01:56 <kmc> (and vice versa)
02:01:59 <kmc> but this is not true for pushdown automata
02:02:09 <kmc> nondeterministic pushdown automata are strictly more powerful than deterministic ones
02:02:31 <kmc> but it is true for turing machines
02:02:43 <Arc_Koen> 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 <kmc> (until you start talking about the execution time rather than just what's possible or impossible)
02:03:09 <kmc> which thing did wikipedia try to explain?
02:03:29 <Arc_Koen> why you couldn't turn a nondeterministic pushdown automaton into a deterministic one
02:03:43 <kmc> yeah, i don't remember offhand
02:04:04 <Arc_Koen> 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 <Arc_Koen> (please excuse the weird way my irc client copies links)
02:07:47 <kmc> finding a proof of this is surprisigly hard
02:07:50 <kmc> or maybe i just suck at googling it
02:07:52 <kmc> http://cstheory.stackexchange.com/questions/9673/why-is-non-determinism-push-down-automata-necessary
02:13:04 <Arc_Koen> so in their example they say you have a word as input
02:13:25 <Arc_Koen> 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 <kmc> a finite state machine or pushdown automaton processes one character at a time
02:28:15 <kmc> 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 <kmc> (of course you can make a machine which rejects all words bigger than n)
02:28:41 <Arc_Koen> hmmm but does it have to process the next character at every tick?
02:28:52 <kmc> a deterministic automaton yes
02:29:40 <kmc> in some presentations, a nondeterministic automaton can have "ε transitions" which move from one state to another without consuming a character
02:29:51 <kmc> but this is a just notational convenience
02:30:27 <kmc> because you could just add everything reachable from ε transitions to the set of possible next states
02:30:56 <kmc> a good book on this stuff is _Introduction to the Theory of Computation_ by Sipser
02:31:16 <kmc> it presents everything in order using consistent notation etc
02:31:30 <kmc> much nicer than reading a bunch of wikipedia pages
02:31:57 <Arc_Koen> yep I definitely should read books
02:35:03 <Arc_Koen> but still, if there are an infinity of possible words
02:35:51 <Arc_Koen> oh, right, you said the epsilon thing was only for nondeterministic automatons
02:38:01 <kmc> actually i'm not sure the ε transitions can be removed from a NPDA
02:38:16 <kmc> you can use them to push or pop more than one stack character per input character
02:38:56 <Arc_Koen> on a dpa with a finite number of states I'm pretty convinced it cannot be removed
02:39:12 <kmc> the set of states is always finite
02:39:35 <kmc> i mean it's not impossible to talk about infinite number of states
02:39:40 <kmc> but it's not what people usually talk about
02:39:44 <Arc_Koen> so where exactly does the "finite-state automaton" name come from?
02:39:58 <kmc> there are a finite number of states
02:40:06 <kmc> i.e. a finite amount of state
02:41:38 <Arc_Koen> 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:51 <kmc> a pushdown automaton also has an infinite number of states icluding the stack
02:43:26 <kmc> (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:33 <Arc_Koen> 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 <kmc> yeah exactly
02:48:23 <zzo38> 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 <Arc_Koen> a half-dragon? I thought we called them lizards
02:51:09 <zzo38> This is different half dragon though.
02:51:23 <Arc_Koen> 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 <Arc_Koen> (as in, losing against a half-dragon implies you would have lost against a whole dragon as well)
02:53:38 <zzo38> I don't think it would imply; it depend how the cards are dealt.
02:54:44 <zzo38> As well as on how good you are at the game.
02:55:37 <Arc_Koen> 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:26 <zzo38> It is a card game, so there would be chance involved, but skill is also involved
02:56:48 <zzo38> No, it is not Zork. It is what I wrote in my character background story for Dungeons&Dragons.
02:57:19 <itidus21> 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 <itidus21> but i dont want to interrupt right now
02:58:26 <zzo38> itidus21: Play by cards?
02:59:01 <itidus21> like the boxing and the basketball
02:59:55 <itidus21> i was thinking more of having a GM
03:00:34 <Arc_Koen> (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 <zzo38> Sure you could, but I would think it would be better by cards
03:01:27 <zzo38> 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 <Sgeo> I'm tempted to just stick with Eclipse
03:01:46 <Arc_Koen> zzo38: well, a box tournament then
03:03:12 <Arc_Koen> 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 <itidus21> is this like playing chess against a wookie?
03:04:39 <Arc_Koen> 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 <Arc_Koen> like, you send the card you want to play along with the letter
03:05:01 <itidus21> well not chess.. i don't know what the actual game is called
03:05:21 <zzo38> Arc_Koen: OK, if you prefer that way.
03:05:42 <Arc_Koen> 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 <itidus21> i see, a dragon is not like a wookie
03:15:16 <Arc_Koen> oh I had an idea for a nondeterministic language today
03:15:31 <Arc_Koen> basically it would be a monopoly-like board game
03:15:56 <Arc_Koen> where all the players are controlled by the computer, with dice being rolled
03:16:20 <Arc_Koen> 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:10:51 <HackEgo> 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:19:26 <kmc> !@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!@!
04:27:27 <ion> > (intercalate " " . map (flip (replicate 'q'))) [1..]
04:27:28 <lambdabot> Couldn't match expected type `GHC.Types.Int'
04:27:38 <ion> > (intercalate " " . map (flip replicate 'q')) [1..]
04:27:40 <lambdabot> "q qq qqq qqqq qqqqq qqqqqq qqqqqqq qqqqqqqq qqqqqqqqq qqqqqqqqqq qqqqqqqqq...
04:28:06 * ion remembers unwords
04:35:57 <Arc_Koen> 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 <Arc_Koen> (that thought was sponsored by the It Is 6 am And I Havent Slept Yet industry)
04:39:50 <kmc> head llac optimization
04:40:50 <kmc> has there been much work on esoteric quantum programming languages
04:41:42 <kmc> there is quantum brainfuck at least
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 <Arc_Koen> well my interrogations about turing-completeness and input/output were legitimate I think
05:52:49 <Arc_Koen> consider a language which has a function "print" and a function "read" which allow to output and input some stuff
05:53:10 <Arc_Koen> and it also has other functions, and considering those other functions only you manage to prove it turing-complete
05:53:49 <Arc_Koen> then someone asks you to write a program in that language that takes an input n, and outputs fib(n)
05:54:33 <Gregor> And? Claiming that a language is TC does not claim that it is possible to do that.
05:55:44 <Arc_Koen> well, I thought turing-completeness was a way to describe what algorithms the language could implement
05:56:20 <Arc_Koen> 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 <Gregor> 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 <Gregor> It can give you fib(n)
05:56:46 <Gregor> The question of how you get “n” is different.
05:57:19 <Arc_Koen> it can ran computations, but it has no ways of giving me a result
05:57:38 <Gregor> So long as it's calculated that result, it's done.
05:57:53 <Gregor> Your disagreement is irrelevant, you're simply wrong.
05:58:07 <Arc_Koen> whoa that's really interesting talking with you
05:58:20 <Arc_Koen> 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).
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:08:29 <Sgeo> How much of a memory hog is Eclipse, exactly?
07:15:44 -!- ion has quit (Ping timeout: 252 seconds).
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 <fizzie> `welcome guy_who_maybe_should_speak_English
07:41:36 <HackEgo> 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:43:53 <lambdabot> *** "floozie" wn "WordNet (r) 3.0 (2006)"
07:43:54 <lambdabot> n 1: a prostitute who attracts customers by walking the streets
07:43:54 <lambdabot> [syn: {streetwalker}, {street girl}, {hooker}, {hustler},
07:44:10 <itidus21> 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 <ais523> 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:39 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: ``: not found
13:04:51 -!- xiaoding has joined.
13:04:56 -!- xiaoding has left.
13:07:03 <dajfsa> ais523: how about {x,y}
13:07:15 <dajfsa> former is probably my favourite although {} are often overloaded for other purposes
13:07:20 <dajfsa> <x,y> is also an option
13:07:26 <dajfsa> [x,y] i find ugly for tuples, (x,y) i find ugly for lists
13:07:38 <dajfsa> ais523: however i would question what your distinction between list and tupl eis
13:07:45 <dajfsa> & if such an overloaded literal actually makes sense given that
13:08:01 <dajfsa> qqqqQQqqqQ*$(@(##(@#*(@#*(@#*(@*(*(@((@~)------------oooooooooooooooooooooooooo===>>>>>>$>$>$>$>$
13:09:03 <dajfsa> nice rant by arc_koen in the logs
13:10:59 <dajfsa> zzo38: what is the internet
13:12:55 <zzo38> dajfsa: Internet is the TCP/IP computer network connected by everything.
13:18:27 -!- atriq has joined.
13:26:34 -!- kinoSi has quit (Read error: Connection reset by peer).
13:27:01 -!- kinoSi has joined.
13:34:45 -!- Taneb has quit (Ping timeout: 248 seconds).
13:35:58 <zzo38> 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 <atriq> zzo38, isn't that in Control.Monad.Cont?
13:37:37 <zzo38> 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:38:07 <atriq> I still haven't understood call/cc
13:38:45 <zzo38> Read the Wikipedia it describe. The esolang wiki article for Unlambda also links to some related information.
13:39:53 <HackEgo> 2011-07-23.txt:00:17:06: <oerjan> very like a whale
13:40:16 <HackEgo> 2010-12-26.txt:05:18:39: <Quadrescence> rms doesn't quite give the same air as jimbo wales
13:40:36 <HackEgo> 2012-09-22.txt:13:40:29: <itidus21> `log wails
13:40:56 <HackEgo> 2012-09-22.txt:13:40:29: <itidus21> `log wails
13:41:07 <HackEgo> 2012-09-22.txt:13:40:56: <HackEgo> 2012-09-22.txt:13:40:29: <itidus21> `log wails
13:41:39 <HackEgo> 2007-11-30.txt:20:08:20: <ihope> Giving the old ones energy would make them temperature wells; creating and destroying particles would make them pressure wells.
13:41:57 <HackEgo> 2009-10-15.txt:13:52:21: <ehird> [The walls, of which there aren't any, melt.]
13:42:11 <HackEgo> 2012-04-20.txt:02:44:02: <elliott> you wills ee
13:42:28 <atriq> In other news, I've finally installed the Haskell Platform correctly on this computer with GHC 7.*
13:48:42 <atriq> 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 <dajfsa> 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:06 <atriq> I'm going to go and read a book
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 <dajfsa> Dog dog dog dog dog dog dog dog dog
16:23:05 <JaBoJa> Cat cat cat cat cat cat cat cat cat
16:24:28 <fizzie> Cat dog cat dog cat dog cat dog cat
16:29:15 <kmc> nice, i made a program that dies with ETOOMANYREFS
16:29:35 <kmc> this errno is only produced in one place in the entire Linux kernel
16:31:56 -!- Vorpal has joined.
16:40:21 <JaBoJa> dog dog dog dog dog dog dog dog
16:40:31 <kmc> dong dong dong dong dong dong dong dong
16:40:55 <JaBoJa> fish fish fish fish fish fish fish fish fish
16:41:10 <kmc> Buffalo buffalo Buffalo buffalo buffalo buffalo Buffalo buffalo.
16:41:42 <JaBoJa> 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 <atriq> 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: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:17 -!- dajfsa has quit (Quit: Lost terminal).
19:06:33 <oerjan> 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 <atriq> 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 <kmc> 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 <oerjan> kmc: wow. i think this is actually quite big.
21:18:34 <shachaf> kmc: roconnor was just talking about that at his talk the other day.
21:18:40 <shachaf> He did some of it, I think.
21:20:51 <oerjan> well he's listed in the sidebar of that page...
21:21:43 <oerjan> not directly related though
21:22:03 <shachaf> Galois Connections, Poset-Enriched Categorical Logic, and Type Theory
21:23:37 <oerjan> 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 <oerjan> although of course the more difficult, too
21:27:12 <ais523> 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:49 <Gregor> Should I buy an accordion?
21:36:14 <atriq> Are you able to play the accordion, or are you able to get accordion lessons?
21:36:30 <Gregor> I am able to play the piano and various other instruments, and am not incompetent.
21:36:40 <atriq> Then the answer is hell
21:37:04 <atriq> Hey, it was your idea
21:37:17 <atriq> Also, go to anime conventions dressed as an esolang
21:37:25 <oerjan> kmc: thanks for giving me my first r/math post, btw :P
21:37:44 <atriq> (should totally be a thing that happens)
21:37:47 <oerjan> actually, first reddit post whatsoever
21:38:24 <shachaf> Feit-Thompson theorem has been, like, TOTALLY checked in Coq
21:38:55 <atriq> My first reddit post was a Muse/Sweet Bro and Hella Jeff mashup on /r/homestuck/ that received one downvote and no comments
21:42:37 <atriq> 8 notes on Tumblr, though!
21:42:53 <ais523> 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 <atriq> When me posting a screenshot of a tweet got 12...
21:44:33 <shachaf> kmc: I watched some episodes of that television series.
21:44:39 <kmc> which one?
21:44:50 <kmc> Poset-Enriched Categorical Logic: The Television Series?
21:45:31 <kmc> are you watching it from the beginning?
21:45:42 <shachaf> 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 <atriq> I think I've just blown someone's mind by playing along with someone else's joke
22:05:37 <atriq> We've convinced her that Power Rangers was originally a British series
22:05:40 <atriq> And that it was awful
22:11:18 <kmc> power rangers is actually a spinoff of dr. who
22:12:30 <olsner> power doctors, doctor rangers, ranger who
22:12:39 <kmc> '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 <kmc> you really cannot make this show sound more awful than it actually is
22:16:16 <Sgeo> I liked Power Rangers when I was a kid.
22:16:33 <Sgeo> Although I think I did recognize how repetitive it is
22:16:34 <olsner> alien "wizard", recruits teenagers, fights evil space aliens... that's doctor who indeed
22:17:14 -!- monqy has joined.
22:28:09 <shachaf> 15:27 <Puffton> If you guys were to explain monads to a newbie, how would you do it?
22:28:28 <shachaf> I should probably leave now. :-(
22:38:49 -!- nooga has quit (Ping timeout: 246 seconds).
22:45:22 -!- segorev has joined.
22:50:00 <HackEgo> 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:51:29 <atriq> We also talk about: maths, Haskell, Homestuck, Dwarf Fortress, Finland, television, Gregor's taste in clothes and accessories...
22:51:55 <shachaf> Is Hexham a kind of Finland?
22:52:09 <Gregor> My taste in clothes is AMAZING, TYVM.
22:52:21 <atriq> Hexham's a kind of Dwarf Fortress
22:52:33 -!- benuphoenix has joined.
22:52:35 <shachaf> Is television a kind of maths?
22:53:26 <olsner> can you own kinds of maths?
22:53:28 <Gregor> Television /involves/ math :)
22:53:57 <olsner> You wouldn't steal a kind of maths!
22:54:17 <segorev> Television and math? Is this stuff compatible?
22:55:02 <benuphoenix> 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:33 <Sgeo> How much would it cost to buy the additional RAM separately?
22:56:07 <ion> Is that ECC RAM or something? Because normal DDR3 RAM is *much* cheaper than that.
22:57:06 <oerjan> <benuphoenix> tggggggggghtjuuy0v= <-- what _is_ with the weird words people use today
22:57:55 <ion> 1333? That’s even cheaper than what i was thinking of.
23:00:07 <benuphoenix> i'm on road. i'll get back to you when i get home
23:00:08 <ion> benuphoenix: In Finland, 16.90 € http://www.verkkokauppa.com/fi/product/15419/cbdjm/Kingston-Valueram-2GB-1333MHz-DDR3-CL9-muistimoduli
23:00:16 <ion> whoops, sorry
23:00:19 <ion> I misread.
23:00:53 <ion> benuphoenix: 19.90 € http://www.verkkokauppa.com/fi/product/4110/dghjq/Kingston-HyperX-blu-4-GB-1600-MHz-DDR3-CL9-muistimoduli
23:01:19 <ion> For some reason, the 4 GiB Valueram 1333 MHz and HyperX 1600 MHz modules have the same price.
23:01:48 <olsner> does byte start with a t in finnish?
23:04:00 <oerjan> they're not big on b's, come to think of it
23:05:44 <olsner> do they even have it at all?
23:06:00 <ion> 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 <kmc> shachaf: television is mostly cardboard and drugs and only a little bit math
23:06:30 <ion> +in school
23:06:52 * shachaf read that as "only a little bit meth"
23:07:00 <kmc> watch more breaking bad
23:09:51 <olsner> "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:42 <atriq> What's a ridiculous Finnish word that everyone should know?
23:12:55 <ion> Yliesierikoisapulaisvaravaurioraivausvuorovarausratkaisupäällikkö
23:13:09 <atriq> ion, what does that mean?
23:14:05 <atriq> Google reckon's it's probably Finnish for something but has no idea what
23:14:27 <olsner> you need to add spaces to help it parse out the words in the word
23:14:41 <ion> 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 <ion> (“pre-special”, huh?)
23:15:50 <olsner> but you're the finnish person here, you should know right?
23:16:17 <ion> I know what it means in Finnish but i’m not familiar enough with title jargon in English.
23:16:35 <atriq> shachaf, there's about half a dozen finns online at any one time
23:17:30 <ion> Okay, the proper translation for esi- in this case would be fore-, not pre-.
23:18:30 <ion> 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 <ion> I mean, the esi-
23:18:44 <olsner> yliesi is like over-pre-something?
23:19:35 <atriq> Isn't it about half two in the morning in Finland
23:19:38 <lambdabot> Local time for ion is Sun, 23 Sep 2012 02:19:38 +0300
23:19:51 <atriq> THAT MEANS GOODNIGHT
23:19:53 -!- atriq has quit (Quit: Leaving).
23:20:11 <olsner> why did he quit because it is late in finland?
23:20:33 <oerjan> sure, everyone knows hexham is in finland
23:20:38 <ion> Here’s a long single word. The previous one was a compound word. kumarreksituteskenteleentuvaisehkollaismaisekkuudellisenneskenteluttelemattomammuuksissansakaankopahan
23:21:10 <olsner> why is that not compound? is it all suffixes and conjugations?
23:22:02 <olsner> looks like it breaks google translate somehow, maybe they have a finnish parser that is actually trying to parse the word
23:23:03 <oerjan> doesn't google translate work purely statistically with no builtin language knowledge?
23:24:51 <olsner> oh well, I took the time to rate this translation "unhelpful"
23:29:17 <oerjan> Phantom_Hoover: it's probably written in a brainfuck derivative
23:29:49 <olsner> there should be a Gerbil Space Program
23:30:03 <oerjan> it's a little known fact
23:30:27 <oerjan> the greatest success of the gluing things to skateboards principle
23:30:36 <olsner> thinking about it, wouldn't gerbils need practically just as big rockets to get into orbit as the human space program?
23:31:39 <oerjan> i thought the size of the rocket would be proportional to the mass of the payload
23:33:01 <olsner> 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 <olsner> oh, apparently the average adult gerbil weighs about 70 g ... they're a lot more smaller than I thought
23:35:21 <oerjan> olsner clearly has been thinking of gerbils as fearsome human-sized monsters
23:37:47 <benuphoenix> which is better: intel h67 chipset or intel b75 chipset?\
23:40:27 <benuphoenix> Sgeo, ion, oerjan? Continuing conversation from before...
23:44:23 <Sgeo> I can tell you which language I'm currently mostly interested in: Clojure. This is completely unhelpful for your question, though.
23:45:20 <benuphoenix> oh...h67 is sandy bridge and b75 is ivy bridge
23:45:31 <shachaf> Sgeo: Wait, you're interested in Clojure?!
23:47:11 <Sgeo> (dotimes [n 500] (println "Yes, shachaf."))
23:47:22 <olsner> oerjan: yes, something like http://en.wikipedia.org/wiki/Josephoartigasia_monesi
23:47:26 <shachaf> benuphoenix: You want Haswell, dude.
23:47:35 <Sgeo> shachaf, what's wrong with Clojure?
23:48:17 <olsner> (no, actually I was just thinking approximately rabbit-sized)
23:50:11 <oerjan> olsner: so not like these, then? http://www.webcomicsnation.com/shaenongarrity/narbonic_plus/series.php?view=archive&chapter=14370
23:55:39 <olsner> assuming the gerbils were also working on this in the '60s, they'd need about a thousand gerbils' weight in computers