00:00:18 -!- augur has quit (Remote host closed the connection).
00:01:24 -!- shikhin_ has joined.
00:04:11 -!- shikhin__ has quit (Ping timeout: 260 seconds).
00:17:05 -!- Phantom_Hoover has quit (Ping timeout: 248 seconds).
00:17:31 -!- yorick has quit (Read error: Connection reset by peer).
00:30:29 -!- fungot has quit (Ping timeout: 248 seconds).
00:31:54 <oerjan> wtf rain
00:32:09 <oerjan> fizzie: halp
00:32:59 * oerjan is happy this downpour didn't happen earlier this evening when he was outside
00:34:47 -!- augur has joined.
00:36:11 -!- shikhin__ has joined.
00:37:38 -!- shikhin_ has quit (Read error: Operation timed out).
00:38:12 -!- shikhin has joined.
00:38:16 -!- ais523 has quit.
00:38:17 -!- shikhin has quit (Changing host).
00:38:17 -!- shikhin has joined.
00:38:39 -!- Sprocklem has joined.
00:41:17 -!- shikhin__ has quit (Ping timeout: 268 seconds).
00:41:37 -!- shikhin_ has joined.
00:42:46 -!- Sgeo has joined.
00:44:21 -!- shikhin has quit (Ping timeout: 248 seconds).
00:46:10 -!- shikhin__ has joined.
00:46:47 -!- shikhin_ has quit (Read error: Operation timed out).
00:57:49 -!- shikhin_ has joined.
00:59:49 -!- shikhin__ has quit (Ping timeout: 248 seconds).
01:03:55 -!- shikhin__ has joined.
01:06:35 -!- shikhin has joined.
01:06:35 -!- shikhin_ has quit (Ping timeout: 248 seconds).
01:08:49 -!- shikhin__ has quit (Ping timeout: 248 seconds).
01:20:52 -!- shikhin has quit (Ping timeout: 264 seconds).
01:22:02 -!- shikhin has joined.
01:43:21 -!- Sprocklem has quit (Ping timeout: 245 seconds).
01:49:47 <Sgeo> "Stock market crash kills 49"
01:51:41 -!- Bike has quit (Ping timeout: 245 seconds).
01:52:28 <kmc> the US government tends to value human life around $6M - $9M
01:52:46 <kmc> so if the stock market destroys $500M of value then I guess that's as bad as killing 49 people
01:52:59 <kmc> of course it's hard to say how much value is really destroyed (or created!) from a huge notional shift in prices
01:53:58 <Sgeo> http://www.youtube.com/watch?v=7Sw9Fh6uk4Q
01:54:58 <kmc> also in a country where your healthcare is tied to your job, it's pretty easy for a stock market crash to directly result in people dying
01:55:34 <Sgeo> :(
02:04:21 -!- Bike has joined.
02:25:05 -!- Sprocklem has joined.
02:39:05 -!- impomatic has left.
02:51:26 * pikhq has apartment. is good
03:13:03 -!- sebbu2 has joined.
03:13:39 -!- augur_ has joined.
03:15:46 -!- augur has quit (Disconnected by services).
03:15:53 -!- augur_ has changed nick to augur.
03:17:19 -!- nisstyre has joined.
03:21:37 -!- rodgort` has joined.
03:22:33 -!- lambdabot has quit (*.net *.split).
03:22:34 -!- sebbu has quit (*.net *.split).
03:22:34 -!- yiyus has quit (*.net *.split).
03:22:34 -!- rodgort has quit (*.net *.split).
03:22:34 -!- ggherdov has quit (*.net *.split).
03:22:34 -!- aloril_ has quit (*.net *.split).
03:22:34 -!- FireFly has quit (*.net *.split).
03:22:35 -!- glogbackup has quit (*.net *.split).
03:24:58 -!- FireFly has joined.
03:25:18 -!- yiyus has joined.
03:25:49 -!- aloril_ has joined.
03:47:02 -!- shikhin has quit (Ping timeout: 240 seconds).
04:47:57 -!- Sprocklem has quit (Ping timeout: 268 seconds).
04:54:53 -!- conehead has quit (Quit: Computer has gone to sleep.).
04:56:52 -!- Bike has quit (Ping timeout: 264 seconds).
05:03:03 -!- Bike has joined.
05:03:49 <Sgeo> In case anyone wants to know what your browser does with https sites with revoked certificates:
05:03:50 <Sgeo> https://lavabit.com/?8-oct-2013
05:04:08 <Sgeo> Chrome won't let me past
05:19:45 <oerjan> assuming you cannot fake a revocation for someone else (a tall assumption, i know) that seems reasonable - the genuine site owner has no reason to use the old one, so it's essentially _sure_ to be malicious.
05:24:16 -!- ggherdov has joined.
05:26:36 -!- asie has joined.
05:26:40 <fizzie> Huh.
05:27:35 -!- fungot has joined.
05:29:54 -!- asie has quit (Client Quit).
05:30:41 <coppro> fizzie: what kind of "r" is the finnish one?
05:30:51 <coppro> I know it rolls, but where
05:31:17 <Bike> http://www.w3.org/Graphics/SVG/WG/track/issues/2071 haha what the christ
05:46:01 <fizzie> I believe it's "officially" an alveolar trill, the plain IPA /r/. I don't know how to describe it in more detail.
05:46:57 <Bike> http://atashi.org/disorientation/ i feel this sums up my svg experience, somehow
05:47:18 <fizzie> (Have to go, bus to catch.)
05:51:22 <kmc> Bike: wow
05:51:43 <kmc> there was a more recent issue (published at Black Hat this year) relating to timing attacks on SVG filters applied to cross-domain iframes
06:04:49 -!- oerjan has quit (Quit: leaving).
06:12:53 <Sgeo> `olist 923
06:12:57 <HackEgo> olist 923: shachaf oerjan Sgeo FireFly
06:13:05 <shachaf> Sgeo: Thanks!
06:13:10 <Sgeo> yw
06:14:28 -!- aloril_ has quit (Ping timeout: 240 seconds).
06:15:24 -!- aloril_ has joined.
06:16:07 -!- Ghoul_ has quit (Ping timeout: 240 seconds).
06:17:27 -!- Tefaj has joined.
06:17:57 -!- Jafet has quit (Ping timeout: 240 seconds).
06:26:40 -!- FireFly has quit (Ping timeout: 240 seconds).
06:27:43 -!- FireFly has joined.
06:31:33 -!- Ghoul_ has joined.
07:03:07 -!- S1 has joined.
07:07:52 <kmc> Diacritical Marks and Peculiar Characters
07:09:58 <fizzie> Is that a children's book? It sounds like one.
07:10:34 <kmc> U+115CE SIDDHAM SECTION MARK WITH RAYS AND DOTTED TRIPLE CRESCENTS
07:10:35 <kmc> http://i.imgur.com/mrT3Aoa.png
07:12:18 <kmc> new in ISO/IEC 10646:2014
07:12:39 <kmc> the Universal Character Set
07:12:41 -!- ^v has quit (Quit: Leaving).
07:14:22 <fizzie> There should be some kind of a project that would extend Unicode (up to some reasonable limit) in all cases where there's e.g. some amount that can vary. For example, the above would immediately lead to SIDDHAM SECTION MARK WITH RAYS AND DOTTED QUADRUPLE CRESCENTS and so on, for (let's say) 1..10 crescents. Both DOTTED and not.
07:15:08 <fizzie> Oh, it exists already.
07:16:06 <fizzie> Oh, it doesn't. It's just the rayless undotted version goes up higher.
07:16:21 <fizzie> Well, there you go, then. All combinations all the time, that's my motto.
07:22:35 -!- S1 has quit (Quit: Page closed).
07:22:38 <kmc> >_>
07:31:35 -!- mnoqy has joined.
07:41:12 -!- kmc_ has joined.
07:43:00 <kmc_> is anyone else having trouble accessing EC2 machines and/or http://amazon.com
07:50:27 <kmc> welp my ISP refuses to talk to amazon for some reason
07:52:37 -!- kmc_ has quit (Ping timeout: 248 seconds).
07:52:49 <kmc> fuck that guy
07:54:49 <shachaf> imo kmc_ > kmc
07:54:59 <kmc> :/
07:55:31 <shachaf> > (compare `on` length) "kmc_" "kmc"
07:55:47 <shachaf> lambdabot more like lambdanot
07:55:55 <shachaf> (the joke is lambdabot is not here)
07:56:37 <shachaf> another joke is that i'm tired
07:56:42 * kmc hugs shachaf 
07:59:37 <shachaf> let's see you say that to my face!!
08:00:11 <kmc> i would...
08:00:25 <shachaf> exactly
08:00:29 -!- FreeFull has quit.
08:00:44 <shachaf> should i move to noe valley
08:00:58 <kmc> hmmmmmmmm
08:01:13 <kmc> why noe valley in particular?
08:01:27 <shachaf> well, the real question is, why noe
08:01:33 <kmc> :D
08:02:05 <shachaf> is it a good place "knows nothing about san francisco"
08:03:28 <kmc> think so
08:14:57 <kmc> san francisco is a good plac
08:14:58 <kmc> e
08:15:10 <kmc> are you looking at an apartment in noe valley
08:15:28 -!- S1 has joined.
08:19:06 <shachaf> i'm not looking at anything right now
08:45:23 -!- S1 has left.
09:11:38 -!- Hyphen-ated has joined.
09:15:59 -!- yorick has joined.
09:23:50 -!- carado has joined.
09:46:43 -!- MindlessDrone has joined.
10:00:34 -!- S1_ has joined.
10:00:39 -!- S1_ has left.
10:12:48 -!- MindlessDrone has quit (Ping timeout: 248 seconds).
10:17:42 -!- carado has quit (Remote host closed the connection).
10:19:46 -!- MindlessDrone has joined.
10:48:51 -!- Taneb has joined.
10:49:00 <Taneb> Hi
10:49:15 <Taneb> I've got an audition this evening
10:53:07 <fizzie> Remember to grip firmly both electrodes of the e-meter.
10:53:33 <fizzie> Oh, audition, not auditing.
10:55:41 <Taneb> The play is apparently a darker version of Jesus Christ Superstar
10:59:02 <mnoqy> ????? how can you be darker than jesus christ superstar
10:59:56 -!- sebbu2 has changed nick to sebbu.
11:01:14 <Taneb> I don't know but they have a pretty big budget
11:13:51 <Taneb> Oh yeah!
11:14:00 <Taneb> I was going to ask you guys a question
11:14:37 <Taneb> I've got an algebraic proof that p | (p & q) == p but it is a bit long
11:16:14 <Taneb> Is there a nice short proof?
11:16:45 <myname> well, make 2 cases :p
11:17:01 <myname> or distibution
11:18:18 <Taneb> I'd rather do it with one case
11:18:29 <Taneb> And my proof with distribution requires ten steps
11:18:33 <Taneb> And I require food, bbl
11:19:03 -!- Taneb has quit (Quit: Page closed).
11:19:20 <myname> 1: p = true: true | x = true, p | (p & q) = true = p
11:19:48 <myname> 2. p = false: false | x = x, p | (p & q) = p & q = false & q = false = p
11:21:28 -!- Sgeo has quit (Read error: Connection reset by peer).
11:39:13 -!- nooodl has joined.
12:13:51 -!- Taneb has joined.
12:30:45 -!- S1 has joined.
12:34:18 -!- S1 has left.
12:36:19 -!- FreeFull has joined.
12:44:43 -!- augur has quit (Remote host closed the connection).
12:45:09 -!- augur has joined.
12:45:19 -!- Taneb has quit (Quit: Leaving).
12:49:31 -!- augur has quit (Ping timeout: 248 seconds).
12:52:06 -!- Koen_ has joined.
13:01:36 -!- boily has joined.
13:03:24 -!- metasepia has joined.
13:05:23 -!- yorick has changed nick to yorickvp.
13:11:45 -!- Phantom_Hoover has joined.
13:18:55 -!- impomatic has joined.
13:20:49 -!- augur has joined.
13:27:47 -!- Taneb has joined.
13:43:13 -!- Taneb has quit (Quit: AndroIRC - Android IRC Client ( http://www.androirc.com )).
13:45:47 -!- carado has joined.
13:51:19 -!- sebbu2 has joined.
13:54:51 -!- sebbu has quit (Ping timeout: 260 seconds).
14:00:01 -!- Taneb has joined.
14:20:18 <Bike> kmc: http://www.thestar.com/news/gta/2013/10/09/foot_soldier_declares_war_on_sanctimonious_cyclists_dimanno.html "For you to read with a straight face"
14:22:25 <mnoqy> i didnt manage
14:22:42 -!- sebbu2 has changed nick to sebbu.
14:23:47 <boily> I thought there weren't bike lanes in the big T.
14:26:22 <Taneb> I managed to read that with naught but a single isolated smirl
14:31:57 <boily> Phantom_Hoover: can I ~duck smirl?
14:32:23 <Phantom_Hoover> oh all right
14:32:28 <Phantom_Hoover> just this once, you understand
14:37:00 -!- conehead has joined.
14:37:16 <Phantom_Hoover> Taneb, also i started a new fortress on a glacier
14:37:22 <Taneb> :O
14:37:32 <Phantom_Hoover> so far it's been p. boring so i'm planning on piping the magma sea over it
14:38:37 <Phantom_Hoover> dunno if i'll have the wood for the reactors though
14:40:44 <boily> Phantom_Hoover: thanks!
14:40:46 <boily> ~duck smirl
14:40:46 <metasepia> --- No relevant information
14:41:03 * boily kicks ~duck in the duckads.
14:41:22 <Taneb> Phantom_Hoover: use caverns to get wood
14:41:41 <Phantom_Hoover> there's no coal here either
14:41:44 <Taneb> If you have access to sand you can use three wood to make a screw pump
14:41:54 <Phantom_Hoover> i'd need steel and a standing military to get into the caverns safely
14:41:55 <Taneb> A magma-safe one, at that
14:42:09 <Phantom_Hoover> i'm on a glacier, Taneb.
14:42:14 <Phantom_Hoover> i don't have access to sand
14:42:23 <Taneb> Trade for it?
14:42:42 <Phantom_Hoover> i have plentiful iron, i'll use that for the pump stack itself
14:43:26 <boily> that sounds like a weird crossover between minecraft, DF and catan...
14:43:46 <Taneb> boily: it is, in a 0:1:0 ratio
14:44:40 <Taneb> I need to work on my fortress
14:44:51 <Taneb> But my computer is a couple of miles away
14:45:09 <Phantom_Hoover> i should've modded anthracite in again...
14:45:18 <Taneb> And I need to practice for my audition in an hour and a half
14:50:25 <Taneb> I need to set an ssh server on my computer and figure out how to get to it from here
14:50:51 <Taneb> Actually, is there any way I could play DF graphically remotely?
14:51:07 <Taneb> Preferably installing as little as possible on the client PC
14:52:02 <boily> can you do X11 forwarding with putty?
14:52:07 <Phantom_Hoover> you could— yeah, that
14:52:14 <Phantom_Hoover> could even use dfhack i guess?
14:52:32 <Phantom_Hoover> (dfhack is now absolutely mandatory btw, it incorporates a heap of unofficial bugfixes)
14:53:01 <Taneb> dfterm looks promising
14:54:02 <myname> dfhack didn't work without x, did it?
14:57:09 <Taneb> Huh, dfterm is written in Haskell
14:57:09 -!- Sprocklem has joined.
14:57:34 <myname> it is, but it spawns df in a new window iirc
14:57:47 <myname> ah, dfterm
14:57:48 <myname> nvmd
14:58:03 <Taneb> I'll see if I can set that up tonight
14:58:48 <myname> not in aur :(
14:59:01 <Phantom_Hoover> myname, dfhack works on windows and in general works by adding hooks to libSDL, so...?
14:59:24 <myname> hm?
14:59:32 <myname> i want to play df via ssh
15:01:28 -!- Sprocklem has quit (Ping timeout: 240 seconds).
15:01:55 <fizzie> Windows X servers are the bests.
15:02:19 -!- JWinslow23 has joined.
15:02:37 <fizzie> The university had a campus-wide license to one of the proprietary ones, possibly Exceed. Not sure if they still do.
15:02:48 -!- Sprocklem has joined.
15:04:50 <JWinslow23> Keep wanting your morning dew...You're my pizza man, my pizza man. I like spastic golden toys. Keep wanting your morning dew... This huge pizza's made with cheese and broccoli!
15:05:00 <JWinslow23> The lyrics of the best song ever!
15:06:14 <boily> Jwinshellow23.
15:06:22 <boily> fungot: do you sing?
15:06:22 <fungot> boily: what's an ircat, i wonder... if i remember what they mean.) poor me.
15:06:39 <JWinslow23> Yes, i do sing!
15:09:24 -!- Sprocklem has quit (Ping timeout: 252 seconds).
15:09:40 <Taneb> Also, I do not like the Python language
15:09:47 <Taneb> I used to, but now I do not
15:10:02 <boily> why the falling out?
15:10:35 <Taneb> Because I didn't touch it for like two years and now I am being forced to
15:10:52 <JWinslow23> ♫♪♩♬♫♪♩♬♫♪♩♬♫♪♩♬♫♪♩♬♫♪♩♬ Everybody sing!
15:10:57 <mnoqy> hi
15:11:14 <Taneb> I can cope, but watching the person next to me debug his code only to find that he had mispelt current_converter halfway down is kinda saddening
15:11:25 <Taneb> Also I couldn't figure out how to serialize data
15:12:04 <boily> JWinslow23: you should get kmc to form a choir.
15:12:07 <boily> Taneb: pickle.
15:12:13 <boily> mnelloqy.
15:12:29 <Taneb> boily: the pickle docs are confusing
15:12:38 <Taneb> `quote Pink Floyd
15:12:44 <HackEgo> 990) <kmc> and then one day you find, ten years have got behind you, no one told you when to run, you missed the starting gun  <kmc> ♫  <kmc> ♫ ♫ ♫  <kmc> (Unicode needs a character specifically for "Pink Floyd guitar solo")
15:13:11 <boily> Taneb: I know I had to serialize data a long time ago. I completely forgot how I managed that.
15:13:28 -!- asie has joined.
15:14:10 <Phantom_Hoover> dammit, the logistics in this fortress are way too fucked to get anything done
15:14:57 <boily> Taneb: if you don't have no binary blobs, you could use json. otherwise, probably something along the lines of protobufs and/or *gasp* ASN.1.
15:17:29 <JWinslow23> `help quote
15:17:30 <HackEgo> Runs arbitrary code in GNU/Linux. Type "`<command>", or "`run <command>" for full shell commands. "`fetch <URL>" downloads files. Files saved to $PWD are persistent, and $PWD/bin is in $PATH. $PWD is a mercurial repository, "`revert <rev>" can be used to revert to a revision. See http://codu.org/projects/hackbot/fshg/
15:17:49 <JWinslow23> `quote Tic Tac Toe
15:17:51 <HackEgo> No output.
15:18:00 <JWinslow23> `quote TicTacToe
15:18:02 <HackEgo> No output.
15:18:08 <JWinslow23> Dang it!
15:20:23 <JWinslow23> `quote Pink Floyd
15:20:25 <HackEgo> 990) <kmc> and then one day you find, ten years have got behind you, no one told you when to run, you missed the starting gun  <kmc> ♫  <kmc> ♫ ♫ ♫  <kmc> (Unicode needs a character specifically for "Pink Floyd guitar solo")
15:21:47 <boily> building out dfterm3. good thing the sandboxes exist in 1.18. fscking stupid de câl*sse de annoying cabal dependency hell de maudit qu'ils sont pas foutus d'avoir réglé ça messemble que c't'évident.
15:22:30 <myname> JWinslow23: is your language specified yet?
15:22:40 <Taneb> Cabal dependency hell it changed the language boily was speaking in
15:23:03 <JWinslow23> Yes, my language is specified.
15:26:09 <Taneb> aaaaaaaaaaaaaah
15:26:16 <Taneb> Audition in less than an hour
15:27:22 <boily> it's only an audition. what can go wrong? (modulo your head suddenly quantum tunneling into an infinity of brainfuck derivatives, but that's easily cured by two Aspirins and a glass of Arcturan mega-water.)
15:28:30 <Phantom_Hoover> what are you auditioning for
15:29:16 <Taneb> Phantom_Hoover: Jesus Christ Superstar
15:30:25 <Phantom_Hoover> are you auditioning for jesus christ
15:30:36 <Taneb> I am just auditioning in general
15:30:49 <Taneb> Although I would not mind recieving the role of Jesus Christ
15:31:44 <myname> JWinslow23: somewhere public?
15:32:31 <Taneb> Phantom_Hoover: if I get the role will you come to York to watch it
15:32:47 <Phantom_Hoover> yes (no)
15:32:52 <Phantom_Hoover> i don't even know where york is
15:33:03 <Phantom_Hoover> if only you had come to birmingham
15:33:17 <Taneb> Do you know where Hexham is relative to Edinburgh?
15:34:01 <Taneb> Because Edinburgh -> York is twice that vector
15:34:02 <Phantom_Hoover> y...es
15:34:23 <Phantom_Hoover> i'm not in edinburgh
15:34:39 <Taneb> Well, do you know where Coventry is relative to Edinburgh?
15:35:24 <Taneb> It's Coventry -> Edinburgh + 2 * Edinburgh -> Hexham
15:36:21 <JWinslow23> Yes, myname, at http://esolangs.org/wiki/Tic_Tac_Toe
15:36:22 <Taneb> hope you like vectors
15:37:17 <myname> so, still a bf derivate
15:37:53 <Phantom_Hoover> wait, york is on the train line i take from coventry to edinburgh
15:38:06 <Taneb> myname: my first language was a bf second derivative
15:38:08 <Taneb> Phantom_Hoover: cool
15:38:20 <JWinslow23> Don't know how to make a stack-based 8 command language to base it off of.
15:38:47 <Taneb> Anyway, I am going to find the audition room now
15:38:51 <Taneb> D/L/036
15:38:55 <Phantom_Hoover> JWinslow23, this seems kind of boring
15:39:36 <Phantom_Hoover> what if you played against some fixed ai or something and its moves corresponded to the executed instructions
15:41:47 <JWinslow23> Sorry.
15:41:50 -!- JWinslow23 has quit (Quit: Page closed).
15:43:38 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...).
15:44:46 -!- Taneb has quit (Quit: Page closed).
16:02:19 -!- Taneb has joined.
16:03:18 -!- Taneb has quit (Remote host closed the connection).
16:03:25 -!- Taneb has joined.
16:04:29 -!- Sprocklem has joined.
16:08:32 -!- asie has joined.
16:08:32 -!- Taneb has quit (Read error: Connection reset by peer).
16:33:28 -!- Sprocklem has quit (Ping timeout: 264 seconds).
16:36:51 -!- shikhin has joined.
16:37:21 -!- Taneb has joined.
16:46:20 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...).
16:50:24 -!- Sprocklem has joined.
16:58:19 <boily> back from lunch, and the espresso was manly.
17:13:22 -!- Phantom_Hoover has quit (Read error: Operation timed out).
17:16:52 -!- ^v has joined.
17:21:12 -!- asie has joined.
17:25:45 <kmc> GNU Make 4.0 is out and it has an embedded Scheme interpreter now: https://lists.gnu.org/archive/html/make-w32/2013-10/msg00021.html
17:27:31 -!- ^v has quit (Ping timeout: 245 seconds).
17:30:16 -!- ^v has joined.
17:31:59 -!- ais523 has joined.
17:33:28 -!- Sprocklem has quit (Ping timeout: 264 seconds).
17:38:33 <ais523> `olist 923
17:38:34 <HackEgo> olist 923: shachaf oerjan Sgeo FireFly
17:39:16 <boily> `pastewisdom
17:39:18 <HackEgo> http://codu.org/projects/hackbot/fshg/index.cgi/file/tip/wisdom/
17:41:25 <boily> @tell oerjan why did you pastold me? (pastelogs + @tell, conflagrated)
17:41:53 <boily> oh. no lambda.
17:43:34 <FireFly> o
17:44:37 <boily> Gregor: ↑ IEEEEEEEEUUUUUUUAAAAAAAAAAAAAAARGHGHGHGHGHGHGHHLHLHLHLHLHLHLHLHL!
17:45:03 <boily> (that was the Sound of the Stance of the Caribou, the Deadliest Candian-Fu Technique!)
17:50:33 <Gregor> Dahell?
17:50:37 <Gregor> What are you screaming at me about?
17:51:54 <shachaf> ais523: Sgeo already `olisted.
17:52:13 <ais523> shachaf: yeah but I wasn't here at th time
17:52:14 <shachaf> Maybe we should put something in HackEgo for this case.
17:52:16 <boily> Gregor: aren't you the lambdabot channeler, or am I grossly mistaken?
17:52:21 <ais523> shachaf: I did suggest that last tim
17:52:23 <ais523> *time
17:52:58 <shachaf> Yes, the emphasis was on "should". Maybe we *should* do that, like you suggested.
17:53:24 <shachaf> But implementing this sort of thing in HackEgo is annoying.
17:54:56 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...).
17:55:59 <ais523> is glogbot working again yet?
17:57:21 -!- Sprocklem has joined.
18:08:28 -!- ^v has quit (Quit: Leaving).
18:09:22 -!- asie has joined.
18:19:42 -!- Sprocklem has quit (Ping timeout: 252 seconds).
18:19:59 <ais523> proggit are criticising GNU Make for adopting != as an assignment operator
18:20:10 <ais523> I see the logic (= for assignment, ! for shell), but it's still a little amusing
18:20:49 -!- Taneb has quit (Read error: Operation timed out).
18:42:38 -!- Taneb has joined.
18:46:08 <boily> Taneb: were you audited?
18:46:39 <Taneb> Aye
18:46:59 <Taneb> Is it weird that I prefer beer from cans to beer from bottles?
18:49:03 <boily> it is beer. it doesn't matter.
18:49:57 <olsner> Taneb: you prefer what you prefer, not much more to it
18:55:01 <boily> speaking of beer, two days ago I tried a http://brasseursdumonde.com/portfolio-items/seigneur-noir/. it's one fungot of a powerful beer!
18:55:01 <fungot> boily: the general trend of it. i find what rms stands for repellant, and so
18:55:19 <boily> fungot: sadly, he does repel a lot of people.
18:55:19 <fungot> boily: man- i don't want to /write/ on a turing machine, i would get some more men!
18:56:07 <boily> fungot: to get more men: the ambition of about half the world's population. maybe more than that.
18:56:07 <fungot> boily: how old are you if i get it.
18:56:14 <boily> fungot: I'm 24.
18:56:44 -!- ^v has joined.
18:58:16 <shachaf> fungot: how old are you
18:58:16 <fungot> shachaf: it's my sadol, functional language
18:58:32 <shachaf> fungot: is that an esolang? also you didn't answer the question
18:58:32 <fungot> shachaf: i don't really look like a klansman? :) what implementation do you use? is it the same person, at least. :)
19:02:21 <boily> fizzie: how old is the fungot?
19:02:22 <fungot> boily: i see it you could just do some regex magick and replace email addresses with something less readable.
19:02:52 <boily> fungot: email addresses are already unparseable enough as they come.
19:02:53 <fungot> boily: but then again i'm planning to use for searches, or maybe even c) but that is the xml family of standards, many of the more direct translation of lambda calculus
19:03:16 <boily> xml and lambda calculus... now that is an interesting idea.
19:06:13 <olsner> XSΛT
19:11:12 <fizzie> boily:
19:11:12 <fizzie> [2008-08-14 11:42:44] ... fungot [n=fungot@qeq4.kyla.fi] has joined #esoteric
19:11:13 <fizzie> [2008-08-14 11:43:49] < fungot> Hello. I'm a silly bot written in Funge-98, using the STRN, SOCK and FGRN fingerprints, running under RC/Funge-98.
19:11:13 <fungot> fizzie: yes, but is never used. right? doing it the wrong way
19:11:13 <fungot> fizzie: does a difference of fnord and springs with bullets shooting them at different frequencies when struck, iirc.
19:11:41 <olsner> fungot: you are used. all the time.
19:11:41 <fungot> olsner: can you give me more bandwidth or i'll read /dev/ fnord /dev/ kmem
19:11:54 <olsner> fungot: ask fizzie :)
19:11:55 <fungot> olsner: corba is really easy to use. in code like that published in a finnish newspaper. i didn't believe that, with huge gaps in numbering now and then
19:12:13 <fizzie> fungot: That makes it sound like you're going to hack out of your box.
19:12:13 <fungot> fizzie: a thermal camera would be nice if one could these days rely on gcc's tco
19:12:46 <fizzie> fungot: I'm not going to buy you a thermal camera.
19:12:47 <fungot> fizzie: to continue off topic, but for the offensive language, constant references to buggery and grain alcohol...
19:12:58 <fizzie> fungot: Or booze.
19:12:58 <fungot> fizzie: for being irish sounding like a good idea. that happens when you plug a cat into the kitchen, to watch him argue with a lisper.
19:13:08 <olsner> dd if=/dev/fnord of=/dev/kmem
19:14:17 <olsner> fungot: it's generally not considered nice to fnord kmem, btw
19:14:18 <fungot> olsner: ( sorry to mention the commonwealth they tend to like descriptive programs
19:14:46 <fizzie> fungot: You don't even have any soft bandwidth caps, and getting a fatter pipe would cost more money.
19:14:46 <fungot> fizzie: well deewiant thinks the jump in subr should not be multiplied beyond necessity. william of occam
19:14:47 <boily> fungot: we of the commonwealth are descriptive, eh?
19:14:47 <fungot> boily: i was gonna bundle up in srfi form fnord." on the usenet, it's called tv. 3 for two seconds before i can try
19:25:10 <boily> fungot: are you of the Dectrip Faith, by any chance?
19:25:10 <fungot> boily: did al or oleg write one?
19:25:25 <boily> fungot: don't think so, but you never know with the Gropagas.
19:25:25 <fungot> boily: consider that nested combination again. :(
19:25:39 <boily> fungot: oooooh, I see. subtle. very subtle.
19:25:40 <fungot> boily: it's a concatenative ( aka stack based) languages that allow keyword arguments require that they go to the quechua class anymore. /me going to find a hungarian restaurant
19:26:06 <boily> fungot, I love you.
19:31:39 -!- lambdabot has joined.
19:33:12 -!- asie has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz...).
19:35:51 -!- MindlessDrone has quit (Quit: MindlessDrone).
19:49:14 -!- shikhin_ has joined.
19:52:40 -!- shikhin has quit (Ping timeout: 264 seconds).
20:32:37 <kmc> 'I asked some Chromium guys how much of the Pepper API the Flash Pepper plugin used. Their answer was literally "150%."'
20:33:24 <coppro> haha
20:47:05 <olsner> is anything except chromium adopting that pepper api thing?
20:47:34 -!- sebbu2 has joined.
20:49:30 <kmc> no
20:49:44 <kmc> it's basically a bunch of chromium internals exposed as an API
20:50:08 <kmc> so it would be hard for e.g. Firefox to adopt it, and this means we can't implement NaCl either
20:50:12 -!- sebbu has quit (Ping timeout: 240 seconds).
20:50:32 <olsner> oh, is NaCl based on/related to pepper?
20:51:09 <kmc> yep, when code running in NaCl wants to talk to the browser / the outside world, it uses Pepper
20:51:13 <kmc> salt and pepper
20:52:37 <Fiora> so pepper is like the system API and NaCl is the runtime/compiler?
20:52:43 <kmc> yeah
20:52:59 <kmc> anyway some people (disclaimer: i'm not speaking officially on behalf of mozilla {corporation,foundation}, blah blah blah) see Google pushing NaCl over asm.js as an anti-competitive anti-open-web vendor-lockin dick move
20:53:19 <kmc> that said, there is https://github.com/google/pepper.js
20:53:36 <ais523> kmc: do people often assume you're speaking officially on behalf of mozilla?
20:53:36 <kmc> which will compile NaCl code that calls Pepper APIs into asm.js JavaScript that calls the standard Web APIs
20:53:54 <kmc> ais523: no but it seems a prudent disclaimer because I am employed by Mozilla Corporation
20:53:57 <ais523> right
20:54:15 <kmc> anyway I don't know how complete pepper.js is; it certainly sounds like it's not enough to run Flash
20:54:38 <kmc> but mozilla has a way better solution for Flash in the works, which is just to reimplement it in JavaScript
20:54:51 <kmc> http://mozilla.github.io/shumway/
20:54:59 <kmc> it's in FF nightlies now I believe
20:55:01 <kmc> behind a flag
20:55:14 <Fiora> how does its performance compare on like, flash games and animations?
20:55:29 <ais523> yeah, the thing about /this/ Flash replacement is that apparently it's backed by a large enough organization that it might actually succeed
20:55:35 <kmc> yeah, unlike Gnash
20:56:10 <kmc> also it reimplements Flash on top of an open standard and a memory safe language
20:56:13 <kmc> which is cool
20:56:28 <ais523> I don't think GNU have the resources/momentum to do really any more really large projects
20:56:33 <kmc> Fiora: I don't have numbers, but I saw a live demo last week and it was silky smooth on some real games
20:56:41 <kmc> I don't know how cherry-picked the set of games was
20:56:48 <ais523> they struggle to keep both gcc and Emacs under control, and Hurd isn't really going anywhere
20:57:29 <kmc> and I don't know how it does on video (eg YouTube), but I think that shouldn't be hard perf-wise, since you would just send it through to the same code paths that handle <video> tags
20:57:39 <Fiora> I thought there were like, plugins that already did that
20:57:49 <Fiora> like, replaced flash video players with native
20:57:54 <kmc> ooh
20:57:57 <Fiora> just by like, snooping the html or something?
20:57:57 <kmc> do you have a link?
20:58:00 <Fiora> ummm   I don't know
20:58:02 <ais523> kmc: AFAIK, Flash for video streaming is mostly independent of Flash for games/animation
20:58:11 <ais523> like, different formats and everything, just with the same brand name
20:58:14 <Fiora> but I remember, like, a ton of flash video is just something like
20:58:18 <kmc> I've vaguely wanted something like that; or also something that runs Gnash just far enough to get a flv url
20:58:20 <Fiora> <some tags     vidoe="myvideo.mp4">
20:58:24 <ais523> .flv can already be played by a bunch of video players (VLC, for instance)
20:58:28 <kmc> ais523: right
20:58:40 <kmc> Fiora: yeah, sometimes it's easy to get a url from the HTML; sometimes it's hard
20:58:43 <ais523> so the problem's just trying to get past all the obfuscation
20:58:51 <lexande> kmc: do you use youtube-dl?
20:58:51 <ais523> kmc: NoScript's quite good at getting at the URL
20:58:51 <kmc> they can actively obfuscate it, esp. if they want to force some ads or DRM on you
20:58:55 <kmc> lexande: sometimes
20:59:03 <ais523> although not perfect
20:59:05 <kmc> ais523: oh, I didn't know it has that power
20:59:06 <kmc> cool
20:59:17 <kmc> of course the Web APIs are getting DRM now too :(
20:59:27 <Bike> yeah what's going on there exactly
20:59:35 <kmc> i don't know anything about it actually
20:59:38 <ais523> kmc: if you click on a blocked Flash video when the rest of the page is unblocked, it typically gives you the actual URL in the confirmation message
20:59:39 -!- Taneb has quit (Quit: Leaving).
20:59:51 <kmc> other than that people are Pissed Off
20:59:56 <Bike> same.
21:00:03 <ais523> basically they're just providing a standardised API to connect to DRM plugins via HTML, I think
21:00:08 <kmc> where again people = some people, not speaking officially on behalf of my employer
21:00:15 <Fiora> hearing about that really confused me.  like.  are the plugins going to be cross-platform or something?
21:00:24 <ais523> which seems to create some minor problems, without actually solving any problems at all
21:00:32 <ais523> Fiora: nothing's forcing them to be, = most likely no
21:00:59 <Fiora> I'm... confused as to like.  why that is literally any different from how it is now o_O
21:00:59 <kmc> I don't fucking understand why publishers think DRM is worth their time and energy
21:01:04 <kmc> presumably they are not all stupid
21:01:07 <kmc> so I must be missing something
21:01:11 <Fiora> like now there's platform-specific browser plugins and stuff for DRM Things
21:01:25 <Fiora> so I mean, they wouldn't do this unless it somehow was better than that for at least someone (?)
21:01:31 <Fiora> but... this... sounds identical?
21:01:32 <kmc> walled garden app stores, game console locking, software DRM all make business sense to me
21:01:35 <kmc> video DRM does not
21:01:59 <kmc> because it only takes one person to crack it and they can redistribute the clean file effortlessly
21:02:15 <kmc> which is less true for software
21:02:39 <kmc> (and the first two of those are more about making life hard for competitors than making it hard for pirates)
21:02:41 <Fiora> kmc: and for like, live streaming stuff some people will just run a screen capture tool and restream it on ustream or something
21:02:45 <kmc> yep
21:03:55 <ais523> the analog hole is impossible to close, best you can do is some sort of steganography so that you can catch the people who did it
21:04:26 <ais523> and ofc HDMI is 100% broken so you can't even secure the digital hole while retaining compatibility with anyone's existing equipment
21:04:45 <kmc> i watched series 7 of Peep Show from some sketchy video site which had video capture of someone else watching it from the official Channel 4 site
21:04:54 <ais523> (the crypto's weak enough that it got broken simply by collecting enough HDMI players from different manufacturers)
21:05:22 <fizzie> ais523: "Impossible" schmimpossible, you just need some kind of a TPM inside the brain of the vic^Wcustomer, and an end-to-end encrypted path to there.
21:05:55 -!- oerjan has joined.
21:06:55 <oerjan> @messages-loud
21:06:56 <lambdabot> You don't have any messages
21:07:21 <oerjan> <boily> @tell oerjan why did you pastold me? (pastelogs + @tell, conflagrated)
21:07:33 <oerjan> boily: to find out wtf you were responding to
21:08:18 <oerjan> @tell boily to find out wtf you were responding to
21:08:18 <lambdabot> Consider it noted.
21:12:30 <fizzie> Speaking of web technologies, how's Silverlight doing these days? 
21:13:11 <kmc> Netflix may be the only significant user, but they're pretty significant
21:13:22 <ais523> fizzie: Microsoft abandoned it, and stopped telling people to use it
21:13:38 <ais523> Netflix continued using it anyway, but it'd be crazy to use it for any new project
21:14:00 <fizzie> I assume Netflix on Android has nothing to do with it though? 
21:14:03 <kmc> they're the ones pushing DRM in HTML5, I think
21:14:04 <boily> hellørjan. I recognize that I may sometimes have some slight temporary trouble with context and stuff.
21:14:36 <fizzie> (Google Play seems to have started offering music -- in addition to books and apps -- for sale in Finland; that's new.)
21:15:36 <fizzie> (No movies/TV yet.)
21:15:49 <boily> it's that time of the day in the year where every shiny surface conspires to blind you.
21:20:52 <shachaf> yørjan
21:23:39 <oerjan> shallo
21:23:59 -!- yorickvp has quit (Quit: No Ping reply in 180 seconds.).
21:24:06 <shachaf> kmc: http://googleonlinesecurity.blogspot.com/2013/10/going-beyond-vulnerability-rewards.html
21:24:27 -!- yorick has joined.
21:26:09 -!- carado has quit (Ping timeout: 252 seconds).
21:27:26 <elliott> $500 for getting rid of strcats?
21:28:50 <kmc> but they keep the strmouse population under control :<
21:29:08 <fizzie> fungot: Why don't you earn your electricity for once and go do something like the aforementioned? 
21:29:09 <fungot> fizzie: help ps kill i eof flush show ls bf_txtgen
21:29:16 <kmc> shachaf: that's cool
21:29:18 <shachaf> ^style
21:29:18 <fungot> Available: agora alice c64 ct darwin discworld enron europarl ff7 fisher fungot homestuck ic irc* iwcs jargon lovecraft nethack pa qwantz sms speeches ss wp youtube
21:29:30 <kmc> so if I make security improvements to BIND then google will give me some cash?
21:29:51 <kmc> I should bust out my Autoconf auto-hardening code and get rich
21:29:59 <fizzie> Only if it has "demonstrable, positive impact".
21:31:41 <kmc> one idea we've kicked around for Servo is running image decoders, etc. in a NaCl-like sandbox
21:32:27 <kmc> (that is, where we don't rewrite them in Rust)
21:35:20 <olsner> http://cr.yp.to/qmail/qmailsec-20071101.pdf had an exaple of almost exactly that, making a sandbox where a jpeg decoder can only read jpeg from stdin and write data on stdout
21:35:48 <Fiora> kmc: does rust let you call asm or the like for things like DCTs?
21:36:29 <olsner> not NaCl-like though, just a unixy sandbox
21:36:37 <kmc> yeah, Chrome already uses OS sandboxing for a lot of things, but I don't think that will scale up to the levels of parallelism we want
21:37:15 <kmc> i don't really trust that a pile of rlimit etc. calls would work, but Linux has seccomp via prctl(2) for this purpose
21:37:32 <ais523> olsner: is that the prctl sandbox on Linux?
21:37:43 <ais523> that turns off all syscalls but read, write, exit, sigreturn?
21:37:56 <ais523> ah, kmc beat me to it
21:37:56 <boily> siri vs. eliza → http://imgur.com/a/7xvqs
21:38:20 <ais523> I've actually used that at work
21:38:22 <olsner> that pdf was much more interesting for the other points than the one example of a sandbox though
21:38:35 <ais523> had to get the computer technicians to set up a VM with it turned on, for us
21:38:50 <ais523> because the stock Linux builds didn't have that particular prctl enabled
21:38:56 <kmc> Fiora: we have an (undocumented) inline assembly feature, but also you can call any function that complies with the C ABI
21:39:07 <Fiora> ahhhh  so you can just write a cdecl function and call that
21:39:11 <kmc> yep
21:39:17 <Fiora> so it doesn't ,like, insist all your code is safe
21:39:20 <kmc> right
21:40:13 <kmc> in fact Rust has first-class support for unsafe pointers and the like, you just need to be inside an unsafe { ... } block to use them
21:40:45 <kmc> like there's a keyword 'unsafe'
21:40:57 <ais523> yeah, Rust's opinion about unsafe code is similar, in its own way, to Haskell's
21:41:09 <ais523> has to be correctly labelled or the type system bitches at you
21:41:48 <kmc> the approach for doing that in Haskell (Safe Haskell) is new and bolted-on and pretty complicated
21:42:11 <kmc> but yeah
21:42:14 <kmc> they are similar philosophically
21:43:11 <kmc> you can also declare functions with 'unsafe fn' in which case they can only be called from an unsafe { ... } block or another such function
21:43:46 <ais523> hmm
21:43:51 <kmc> so you can import a C library, define an unsafe API (which might still be higher level in some ways), and then provide a safe wrapper where your proof obligation lies at a particular point in the code
21:43:55 <kmc> which is cool
21:44:05 <ais523> can you have unsafe fn arguments?
21:44:21 <ais523> or, well
21:44:22 <kmc> what would that mean?
21:44:30 <ais523> say I want to use "map" from within an unsafe function
21:44:35 <ais523> and give it a unsafe function as a argument
21:44:38 <ais523> *as an
21:44:42 -!- boily has quit (Quit: definitely not chicken. more like tuna.).
21:44:48 <kmc> interesting question!
21:44:48 -!- metasepia has quit (Remote host closed the connection).
21:44:49 <ais523> do I need to create a separate unsafe_map
21:44:50 <kmc> i haven't thought about that
21:44:54 <kmc> I bet you do :(
21:44:55 <ais523> or can map be polymorphic on unsafety?
21:45:18 <ais523> kmc: thinking about this sort of thing is what I do, nowadays
21:45:37 <kmc> we don't have polymorphism over safety, nor over mutability, nor over type constructors even :(
21:45:43 <kmc> ais523: oh? what are you working on?
21:46:08 <ais523> kmc: resource-bounding type systems
21:46:20 <ais523> most recently, attempting to make the type system polymorphic in sharing
21:46:23 <kmc> cool
21:46:27 <ais523> and parallelism
21:46:41 <ais523> like, with the existing type systems, if I want to implement "let" syntactic sugar
21:46:54 <ais523> that binds multiple variables
21:47:08 <ais523> what it desugars to is different depending on whether the variables can execute in parallel, or whether they can share resources
21:47:20 <ais523> (they can't both execute in parallel /and/ share resources, that's the point of the type system)
21:47:34 <ais523> the new type system desugars it consistently in both cases
21:56:12 <kmc> cool
21:56:21 <kmc> what system is this?
21:56:57 <ais523> kmc: the old system is called Syntactic Control of Interference, you can find a bunch of papers about it on Google Scholar
21:57:07 <ais523> the new one is new, and not written up in enough detail to be public yet
21:57:10 <ais523> but it'll be in my PhD
22:00:36 <kmc> cool
22:00:45 <kmc> is it a substructural type system then?
22:01:26 <ais523> I'm not 100% sure on what substructural means, but almost certainly yes
22:01:57 <kmc> ok
22:03:24 <shachaf> what about a structural subtype system
22:03:31 <kmc> that's also a thing yes
22:03:57 -!- conehead has quit (Quit: Textual IRC Client: www.textualapp.com).
22:04:15 <shachaf> the phrase "substructural subtyping" has three results on the google
22:04:24 <shachaf> the first one is about go
22:04:38 <ais523> the language, or the game, or something else entirely?
22:04:57 <ais523> (the healthy-ish fast food chain that supplies Birmingham University, for instance?)
22:05:06 <kmc> in a substructural system you aren't automatically allowed to duplicate / discard / reorder the elements of the type context
22:06:11 <ais523> right
22:06:28 <ais523> going down the tree, or upwards?
22:06:51 <ais523> I don't allow contraction, but I do allow weakening (it's affine, not linear), and banning reordering would be ridiculous outside esolangs IMO
22:07:09 <shachaf> Affine type systems are substructural, sure.
22:07:12 <kmc> yep
22:07:26 <ais523> yeah, it's affine
22:07:45 <ais523> incidentally, does "affine" in general have any meaning other than "linear but not quite"?
22:07:55 <ais523> it's used to mean that in several different contexts
22:08:04 <kmc> Rust has affine types, and the stuff you mentioned with checking non-interference between lets sounds similar to Rust's uniqueness and borrow checkeing
22:08:23 <shachaf> I generally see "affine" used to mean "0 or 1" in some sense or another.
22:08:27 <Koen_> an affine space is like a vector space except we forgot who's zero
22:08:36 <shachaf> Where "linear" is "exactly 1" and "relevant" is "1 or more"
22:09:04 <shachaf> Or maybe I made that up, I don't know.
22:09:19 <ais523> kmc: it's not the same as Rust, but there's a similar spirit there, I think
22:09:23 <kmc> yeah
22:09:27 <shachaf> But I think it works with all the uses I've seen.
22:09:30 <ais523> Rust's aiming to make sure that something isn't deallocated early or late
22:09:34 <kmc> ais523: so do you infer when things can run in parallel?
22:09:45 <ais523> whereas I'm trying to make sure that things aren't copied inappropriately
22:09:48 <ais523> kmc: in theory, yes
22:09:52 <shachaf> there's also a sandwich place at the google called go: http://menu-mtv-go.blogspot.com/ i don't know whether it came before or after the language
22:09:55 <ais523> although in practice, we don't actually have an inference algo yet
22:09:57 <ais523> just the type system
22:10:09 <ais523> (my supervisor wants to just use Z3, though)
22:10:13 <kmc> haha
22:10:22 <kmc> that's awesome
22:10:59 <ais523> IMO using an algorithm specialized for the task is likely to work better
22:11:02 <ais523> but who knows, maybe Z3 would work
22:11:11 <shachaf> you know how there are four properties of relations, "functional", "total", "injective", "surjective"
22:11:19 <shachaf> where a function is a functional total relation
22:11:34 <kmc> is there existing work on implementing type inference with SMT solvers?
22:11:50 <shachaf> a surjective function is a function that maps each element in the domain to at least one element in the codomain
22:11:50 <ais523> kmc: probably not, because at least for Hindley-Milner there's no reason to do so
22:11:57 <shachaf> an injective function is a function that maps each element in the domain to at most one element in the codomain
22:12:18 <shachaf> i'd like to find an excuse to use the words "affine" and "relevant" and "linear" there
22:12:35 <ais523> I'm not convinced your definitions of surjective and injective are correct
22:12:39 <kmc> ais523: sure, most real-world languages with inference go beyond H-M though
22:12:41 <ais523> I think you have the domain and codomain backwards
22:12:49 <shachaf> ais523: Er, yes, I do.
22:13:07 <shachaf> In that direction it's always "exactly 1".
22:13:10 <kmc> Rust has some weird inference corner cases, arising from the fact that we have a *little* bit of subtyping hidden deep down
22:13:25 <shachaf> A relation is total/functional if its opposite relation is surjective/injective.
22:13:28 <ais523> kmc: http://www.cs.bham.ac.uk/~drg/papers/popl11.pdf is my work on inference algorithms
22:13:38 <kmc> cool
22:13:59 <ais523> that's inference for SCC, which is basically a type system where the maximum number of copies of anything that might simultaneously execute is statically known
22:14:12 <ais523> the main result there is that it's decidable, which isn't obvious
22:15:37 -!- shikhin_ has quit (Read error: Operation timed out).
22:19:19 <oerjan> <ais523> is glogbot working again yet? <-- yes
22:19:31 <ais523> thanks
22:19:54 <oerjan> technically most of it always did.  but Gregor said he fixed the formatted logs.
22:21:05 <shachaf> ais523: do you know a good thing to read to learn about linear logic and such
22:21:25 <ais523> shachaf: no, I actually don't understand the whole of linear logic myself
22:21:28 <ais523> I only work with fragments
22:21:50 <oerjan> no one understands par or ?, tru fax
22:22:03 <ais523> although learning categorical semantics helps
22:22:19 <shachaf> what is linear logic even like categorically
22:22:26 <ais523> and the difference between tensors and products (i.e. the monoids of monoidal closed categories, and cartesian closed categories, respectively)
22:22:28 <shachaf> people were talking about it a bit in ##typetheory
22:22:47 <ais523> shachaf: basically for affine, you don't have cartesian closure
22:22:52 <shachaf> oerjan: isn't ?X just "some number of X which is specified by someone else"
22:23:10 <oerjan> shachaf: i have no idea
22:23:13 <ais523> and for linear, your monoid units aren't terminal objects any more
22:23:19 <shachaf> ais523: i like how comonoids become non-boring with linear logic
22:23:48 <ais523> how do the counits work for comonoids?
22:23:59 <ais523> having a bit of trouble mentally reversing the definition
22:23:59 <shachaf> Well, not everything is a comonoid.
22:24:11 <ais523> yeah, I know
22:24:13 <ais523> I'm asking, what are the axioms
22:24:26 <shachaf> Oh.
22:24:31 <ais523> presumably, left and right coidentity, and coassociativity
22:24:47 <ais523> but I'm not entirely sure what those are
22:24:52 <shachaf> Right. I don't know about linear logic in particular but that's what it'd be in general.
22:25:20 <ais523> yeah, but what does a coassociativity axiom look like anyway
22:25:41 <ais523> for a normal monoid, we have (A \otimes B) \otimes C = A \otimes (B \otimes C)
22:25:53 <oerjan> i suppose that makes sense.  !x = 1 & (x * !x) isn't it, so by duality you should have ?x = _|_ + (x par ?x).  oh wait par.
22:26:09 <oerjan> shachaf: there's a par in that, all hope is lost.
22:26:13 <ais523> I'm having trouble even expressing the opposite of that
22:26:27 <ais523> because the arities are all wrong
22:26:28 <shachaf> It's the reverse of the diagram in https://en.wikipedia.org/wiki/Monoid_object
22:27:12 <ais523> shachaf: that diagram is either wrong or doesn't match the text
22:27:16 <ais523> it uses an alpha, exactly once
22:27:31 <ais523> ah no, it's the alpha from the category as a whole
22:27:42 <ais523> thus, that diagram only makes sense for a monoidal category
22:27:43 <shachaf> Yes, it's a monoidal category.
22:27:51 <shachaf> That's how a monoid object is defined.
22:27:58 <ais523> ah right
22:28:02 <ais523> so the category is still monoidal
22:28:09 <ais523> but it has objects which are comonoids?
22:28:26 <ais523> I was trying to mentally work out wtf a coassociative cobifunctor was
22:28:30 <shachaf> Yes.
22:28:46 <ais523> if that concept actually doesn't make sense, it'd explain why I couldn't figure it out
22:29:13 <shachaf> As far as I know comonoids are still defined in a monoidal category.
22:29:18 <ais523> OK, so for a comonoid, I start with one M
22:29:21 <ais523> and explode it to M x M
22:29:30 <ais523> and whichever of those Ms I explode next, I get the same M x M x M
22:29:35 <ais523> (no parens because it's associative)
22:29:36 <shachaf> Then you can expand either M and you get the same thing (after reässociation).
22:29:37 <ais523> where x is an \otimes
22:29:39 <shachaf> Right.
22:29:55 <shachaf> Well, x depends on your choice of monoidal category.
22:29:57 -!- nooodl has quit (Ping timeout: 248 seconds).
22:29:58 <oerjan> cobifunctors sound like something the japanese would invent.
22:30:04 <ais523> shachaf: yeah, but \otimes is the general term
22:30:26 <shachaf> Even in e.g. Haskell you can define monoids/comonoids with (,)/() or Either/Void if you want.
22:30:36 <ais523> right
22:30:41 <shachaf> (But only one of those four combinations is actually interesting.)
22:30:48 <ais523> the categories I've been working with recently are monoidal in two different ways
22:31:03 <shachaf> Oh, you mean \otimes as in tensor product in the monoidal category, not as in linear logic's \otimes?
22:31:12 <ais523> I mean \otimes as tensor, yes
22:31:16 <shachaf> OK, sure.
22:31:34 <ais523> comonoid objects must be much rarer than monoid objects, I think
22:31:45 <ais523> I think I get how they behave, but I'm having trouble thinking up examples
22:31:47 <shachaf> In which category?
22:32:03 <shachaf> In Haskell every type is a ((,)/()) comonoid, of course.
22:32:27 <shachaf> Where counit _ = (), comult x = (x,x)
22:32:53 <ais523> oh right, because the comonoid is "aware" of what type it's operating on
22:32:55 <shachaf> In linear logic, the idea is at least related to !, I think.
22:32:58 <ais523> so it even works on, say, (Int, Int)
22:33:11 <ais523> I start with (2,4), then get (2,4,2,4), and can double either to get (2,4,2,4,2,4)
22:33:19 <ais523> without having to worry about accidentally getting (2,2,4) or (2,4,4)
22:33:40 <ais523> this is one level of abstraction below the one I normally work at
22:33:44 <ais523> which is why I'm confused
22:34:01 <ais523> categorical semantics has too many levels of abstraction :(
22:34:25 <shachaf> Anyway, does linear logic even have products and so on?
22:34:40 <shachaf> Is there a terminal object? What are the arrows, anyway?
22:34:41 <ais523> it has both a product and a tensor, I think
22:35:04 <ais523> full linear logic is what you get when you glue together lots of different type systems
22:35:19 <shachaf> oerjan: is par the upside down &
22:35:39 <oerjan> yes
22:35:46 -!- Phantom_Hoover has joined.
22:35:48 <ais523> it should be called \dna :(
22:35:53 <ais523> * :-(
22:36:53 <ais523> huh, on Wikipedia, [[Categorical semantics]] is a redirect to [[Categorical logic]], which is an overview page linking to [[Categorical semantics]] for the main information
22:37:35 <ais523> <Jpbowen, 6 October 2005> <!-- A separate entry would be better, but this is better than nothing! -->
22:39:44 <ais523> "Construct the set S of solutions in the abstract domain of positive integers formed by quotienting Z^0,+ over the equivalence relation a \equiv b iff a=b \vee (a≥2 \wedge b≥2) […]"
22:40:08 <ais523> in other words, I effectively got to say in a mathematical paper "assume that the only integers are 0, 1, many"
22:41:30 <mnoqy> :D
22:43:38 <shachaf> hi mnoqy do you know about categories and linear logic
22:43:40 <kmc> Fiora: in the vein of "Rust can handle low-level unsafe things" I'll also mention that the Rust runtime system is mostly written in Rust
22:43:52 <mnoqy> shachaf: i know about categories!
22:44:01 <mnoqy> i've never bothered to learn linear logic stuff though
22:44:10 <shachaf> i,i hi mnoqy do you know about categories par linear logic
22:44:10 <kmc> which includes a userspace green-thread scheduler and an implementation of reference counted boxes (and one day, a garbage collector)
22:44:19 <Fiora> what's a green-thread?
22:44:26 <kmc> lightweight userspace threads
22:44:28 <ais523> Fiora: I think it's one that doesn't use the OS threading
22:44:40 <kmc> we map them onto a configurable number of OS threads
22:45:09 -!- mnoqy has quit (Quit: hello).
22:45:28 <kmc> they are preemtible whenever they do IO
22:45:32 <shachaf> non-native userspace green-threads implemented without os support
22:45:41 <ais523> kmc: I was just about to ask about the preëmption rules
22:45:50 <ais523> what if a thread goes into an infinite loop with no IO?
22:45:58 <ais523> (i.e. a tight infinite loop)
22:46:03 <kmc> (so they are less preemptible than GHC threads, which can be preempted on any allocation and these days there's a flag to make them always preemptible)
22:46:11 <ais523> does it block the other threads in its thread block?
22:46:13 <kmc> ais523: then it consumes a whole OS thread
22:46:17 <kmc> I think the others can move around
22:46:21 <kmc> the scheduler is work-stealing
22:46:24 <kmc> I'm not positive, though
22:46:24 <ais523> right
22:46:41 <kmc> (i'm gonna say "task" instead of "green thread" from here on because that's the Rust terminology)
22:47:09 <kmc> also, sending a message to another task will (by default) context switch your thread to that task
22:47:15 <kmc> so they are kind of like coroutines, performance-wise
22:47:20 <kmc> but you can also do a deferred send
22:47:54 <ais523> I like this sort of thing
22:47:59 <ais523> simple semantics, optimized implementation
22:48:17 <kmc> Fiora: so in terms of low level stuff, Rust can basically do anything C and C++ can do, including write a Rust runtime system
22:48:25 <kmc> as long as you don't use the RTS features as you are implementing them :)
22:49:18 <oerjan> ais523: fixed your self-redirects
22:49:33 <ais523> oerjan: on Wikipedia?
22:49:50 <ais523> I was considering fixing it, but it was hard to think of an improvement
22:49:57 <kmc> and if you don't link against the standard RTS, you can implement just the language features you use
22:49:59 <ais523> oh, they were /all/ self-redirects?
22:50:01 <ais523> ouch
22:50:01 <kmc> which looks like http://ix.io/8fH
22:50:29 <kmc> this code uses ~-boxes therefore it's required to provide the exchange_malloc and exchange_free "lang items"
22:50:37 <kmc> which here are just calls to C malloc and free
22:51:11 <kmc> (they are also basically just that in the standard RTS, too, but that's subject to change.  i think they call a statically linked jemalloc)
22:54:24 <oerjan> ais523: i've been thinking mediawiki needs a way to mark pages as "links to here should get a different color" which can be used on things like this, and redirects from misspellings.
22:54:40 <oerjan> but lacking that, i don't know anything better than turning it into bold.
22:54:58 <oerjan> (now you may tell me this feature already exists twh)
22:55:03 <ais523> oerjan: it implements at least two of those (redirects, short pages), but as user preferences
22:55:30 <ais523> a while back, there was a major push at Wikipedia to set the default "short pages" limit at 0 rather than -1
22:55:34 <ais523> and set the color to red
22:55:39 <ais523> so that you could delete a page by blanking it
22:55:40 <oerjan> ais523: well the point would be that it wouldn't apply to _all_ redirects, just ones marked with a certain template.
22:55:43 <ais523> it fizzled out, though
22:55:49 <ais523> oerjan: yeah, that's harder
22:55:55 <oerjan> e.g. i'd apply it to [[Issac Newton]], my old nemesis.
22:56:00 <ais523> although, hmm
22:56:19 <ais523> you could do it by spamming the redirects you wanted to mark with a sufficiently long template
22:56:25 <ais523> and then setting a different color for "redirect, not short"
22:56:34 <oerjan> XD
22:56:35 <ais523> I believe there are a few redirects with long spam comments for that purpose on Wikipedia
22:56:43 <ais523> although I might be wrong
22:56:48 -!- ping has joined.
22:57:12 -!- ping has changed nick to Guest54426.
22:57:35 <oerjan> ais523: it's half useless as a user preference though, since the person who _introduced_ a misspelled link wouldn't see it.
22:57:52 <oerjan> (being they're obviously too stupid to set preferences)
22:57:54 <ais523> oerjan: yeah but everything else in Wikipedia is half useless too
22:57:57 <ais523> so it balances out
22:58:02 <oerjan> OKAY
22:58:02 <ais523> err, in MediaWiki
22:58:56 -!- ^v has quit (Ping timeout: 245 seconds).
22:59:55 -!- Guest54426 has quit (Client Quit).
23:03:00 -!- ^v has joined.
23:11:23 -!- conehead has joined.
23:14:08 -!- Sprocklem has joined.
23:14:12 -!- Frooxius has quit (Quit: ChatZilla 0.9.90-rdmsoft [XULRunner 1.9.0.17/2009122204]).
23:24:46 -!- Frooxius has joined.
23:41:24 -!- yorick has quit (Read error: Connection reset by peer).
23:59:21 -!- Phantom_Hoover has quit (Remote host closed the connection).