You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
sarahzrf (Mar 31 2020 at 14:53):oh yeah, mike's \parr failing to render reminds me that i had to resort to putting a unicode ⅋ in one of my messages
sarahzrf (Mar 31 2020 at 14:54):is there any way to add cmll to the latex environment here?
sarahzrf (Mar 31 2020 at 15:01):oh sheesh i guess probably not https://github.com/zulip/zulip/blob/cfa62700809584003468a982605ef724204a5f21/zerver/lib/tex.py
sarahzrf (Mar 31 2020 at 15:01):maybe i'll open an issue on the github...
sarahzrf (Mar 31 2020 at 15:02):...AAAAAAAAAAAAAA https://github.com/zulip/zulip/blob/243d8ffc5154ac7d52697706c9c6ff3f19a7cc53/zerver/lib/bugdown/fenced_code.py#L366
sarahzrf (Mar 31 2020 at 15:02):what are they DOING :scream:
sarahzrf (Mar 31 2020 at 15:05):why is it legal, in 2020, to write web apps used by tons of people, while still believing that html is a string
Ben Steffan (Mar 31 2020 at 15:10):That's not even the worst offense in that file
Jules Hedges (Mar 31 2020 at 15:10):There's no emoji for Zalgo, have to resort to Cthulhu instead :octopus:
sarahzrf (Mar 31 2020 at 15:20):this is maybe continued off-topic but i kinda want to mention this slightly somewhere:
sarahzrf (Mar 31 2020 at 15:22):one of the like invited/featured talks at POPL '20 was about secure programming languages
sarahzrf (Mar 31 2020 at 15:22):and half or more of the talk was just talking about what existing languages do and stuff
sarahzrf (Mar 31 2020 at 15:22):and half of that was just misinformed or dangerous!
sarahzrf (Mar 31 2020 at 15:23):like it described PHP as "having language support for sanitization" and hence that being a secure language feature :scream:
sarahzrf (Mar 31 2020 at 15:23):or something along those lines
sarahzrf (Mar 31 2020 at 15:23):and it brought up ruby's taint system, despite the fact that afaik nobody ever uses that
sarahzrf (Mar 31 2020 at 15:23):/offtopic
sarahzrf (Mar 31 2020 at 15:24):actually no one more thing:
sarahzrf (Mar 31 2020 at 15:24):never even mentioned templating once
sarahzrf (Mar 31 2020 at 15:24):iirc
Ben Steffan (Mar 31 2020 at 15:25):Let's take this to #off-topic ?
sarahzrf (Mar 31 2020 at 15:27):ok can i now move this topic to another stream, or
Ben Steffan (Mar 31 2020 at 15:28):I thought that was impossible?
sarahzrf (Mar 31 2020 at 15:28)::face_palm:
sarahzrf (Mar 31 2020 at 15:29):well, better it clutters the ct stream than it clutters the ct stream & the bi heyting algebra topic, i suppose
Ben Steffan (Mar 31 2020 at 15:29):Yeah
Ben Steffan (Mar 31 2020 at 15:30):Anyways, have I said that
AHHHHHHHH
Ben Steffan (Mar 31 2020 at 15:31):All of this vaguely reminds me of the Perl talk
sarahzrf (Mar 31 2020 at 15:31):let's actually move this to #off-topic though
sarahzrf (Mar 31 2020 at 15:31):i'll open a new topic there
Ben Steffan (Mar 31 2020 at 15:31):Ok
Stelios Tsampas (Mar 31 2020 at 17:46):sarahzrf said:
and half of that was just misinformed or dangerous!
Huh, really? Lemme get my hands on that presentation and get back to you. Being a (practical) security/formal guy in-betweener I have a feeling this presentation will trigger me.
Also, what's up with that zulip code? Why do the devs ignore so many layers of abstraction?
Ben Steffan (Mar 31 2020 at 17:50):You'd almost think Zulip was a commercial product...
Stelios Tsampas (Mar 31 2020 at 17:54):Believe it or not it's the commercial, closed-source software that suffer the most in terms of bad code.
Ben Steffan (Mar 31 2020 at 17:55):That's essentially what I was alluding to :P
Stelios Tsampas (Mar 31 2020 at 17:58):Gotcha my man! You see zulip is a commercial product so it was hard to tell if the sarcasm was directed to "Zulip" or to "commercial products".
sarahzrf (Mar 31 2020 at 17:58):Stelios Tsampas said:
Huh, really? Lemme get my hands on that presentation and get back to you. Being a (practical) security/formal guy in-betweener I have a feeling this presentation will trigger me.
can you please not use "trigger" flippantly :\
Ben Steffan (Mar 31 2020 at 17:58):Wait, Zulip is commercial? I was not aware of that
Stelios Tsampas (Mar 31 2020 at 17:58):Lemme google "flippantly" first.
Stelios Tsampas (Mar 31 2020 at 17:59):Ben Steffan said:
Wait, Zulip is commercial? I was not aware of that
Yes, they do offer commercial services.
Ben Steffan (Mar 31 2020 at 17:59):Ah well, I guess it makes sense then
sarahzrf (Mar 31 2020 at 17:59):anyway here's the talk https://www.youtube.com/watch?v=dhoP-dyIr54
Stelios Tsampas (Mar 31 2020 at 18:01):sarahzrf said:
can you please not use "trigger" flippantly :\
Hahah, sure! I deserved that :D.
Ben Steffan (Mar 31 2020 at 18:02):Okay, two minutes into the talk and I'm already annoyed, cool
sarahzrf (Mar 31 2020 at 18:10):oh? i didnt think there was too much objectionable that early
sarahzrf (Mar 31 2020 at 18:10):it's nothing too new at that point but not particularly annoying
Ben Steffan (Mar 31 2020 at 18:12):...I forgot what I was annoyed about
sarahzrf (Mar 31 2020 at 18:13):i guess it does get a bit "cmon, just get to the point" when shes like 10 minutes in and going over stuff that's super boilerplate still
Ben Steffan (Mar 31 2020 at 18:14):Yeah, that's definitely annoying
sarahzrf (Mar 31 2020 at 18:14):the presentation seriously felt to me like
sarahzrf (Mar 31 2020 at 18:14):"ok web dev 103 class, time to learn about security"
sarahzrf (Mar 31 2020 at 18:15):for a lot of it
sarahzrf (Mar 31 2020 at 18:15):\>.>
Ben Steffan (Mar 31 2020 at 18:15):Ah, I think I was already annoyed about the motivation at the start. Like, the numbers she presented just don't seem that high to me?
sarahzrf (Mar 31 2020 at 18:15):i mean, wasnt she talking about holes in pieces of software, not just particular intrusions
Ben Steffan (Mar 31 2020 at 18:15):5 new exploits per day, over _all_ the software that is registered with that particular exploit database? That doesn't seem so much tbh
sarahzrf (Mar 31 2020 at 18:16):actually yeah taht does sound kinda low
Ben Steffan (Mar 31 2020 at 18:16):Perhaps my sense of scale if off here
sarahzrf (Mar 31 2020 at 18:16):btw on that topic https://fishinabarrel.github.io/
sarahzrf (Mar 31 2020 at 18:17):s t o p u s i n g C
Ben Steffan (Mar 31 2020 at 18:18):I guess I'm also a bit sour about the fact that this is essentially a corporate presentation where every slide has an oracle logo on it
sarahzrf (Mar 31 2020 at 18:18):lol
sarahzrf (Mar 31 2020 at 18:18):welcome to conference land 🤪
Ben Steffan (Mar 31 2020 at 18:18):???
Ben Steffan (Mar 31 2020 at 18:18):That's not the norm for any software conference I know about
sarahzrf (Mar 31 2020 at 18:19):well ok maybe not on the talks
sarahzrf (Mar 31 2020 at 18:19):there were for sure logos on the bags n stuff tho
Ben Steffan (Mar 31 2020 at 18:19):I mean sure lots of people give talks on behalf of company X, but usually they say it once in the beginning and that's it?
sarahzrf (Mar 31 2020 at 18:19):yeah
Ben Steffan (Mar 31 2020 at 18:19):Ah yeah, I guess that's normal
sarahzrf (Mar 31 2020 at 18:19):fair enough, that's a different thing
sarahzrf (Mar 31 2020 at 18:21):welcome to PL, your options are:
Ben Steffan (Mar 31 2020 at 18:21):Love how PHP gets the bonus of "Injection prevention" as a library feature but the other languages don't?
sarahzrf (Mar 31 2020 at 18:22)::100:
Ben Steffan (Mar 31 2020 at 18:22):I'm sure that Java also has that as a library feature but ok
Ben Steffan (Mar 31 2020 at 18:22):...and all the other languages too probs
sarahzrf (Mar 31 2020 at 18:22):not to mention that escaping things is the wrong approach
sarahzrf (Mar 31 2020 at 18:23):"sanitization" is the wrong way to think about things
Ben Steffan (Mar 31 2020 at 18:23):first class support my favourite buzzword!
sarahzrf (Mar 31 2020 at 18:23):cmon now first-class support can be a real thing
sarahzrf (Mar 31 2020 at 18:24):anyway though the fact that PHP encourages you to just pass query strings and interpolate your parameters in
Ben Steffan (Mar 31 2020 at 18:24):first class support has no defined meaning in my book
sarahzrf (Mar 31 2020 at 18:24):when every time ive ever used sql from another language, the interface has let you pass the parameters as separate arguments and it does the interpolation for you
sarahzrf (Mar 31 2020 at 18:24):means that php is more dangerous
sarahzrf (Mar 31 2020 at 18:24):because it puts the escaping obligation on you
sarahzrf (Mar 31 2020 at 18:24):aaaaaaaaaaa
sarahzrf (Mar 31 2020 at 18:28):anyway here's a palate cleanser https://www.youtube.com/watch?v=BDnbxBmwNyQ
sarahzrf (Mar 31 2020 at 18:28):...probably incomprehensible if you don't have a background in formal verification but
sarahzrf (Mar 31 2020 at 18:28):one of the talks i enjoyed the most that i went to ^_^
Ben Steffan (Mar 31 2020 at 18:29):Love how the implication is that Java is slow mainly because of the gc
sarahzrf (Mar 31 2020 at 18:31):is java even very slow
Ben Steffan (Mar 31 2020 at 18:31):It's fairly slow, from my perspective
Ben Steffan (Mar 31 2020 at 18:31):But my perspective is also "compared to C++", so
sarahzrf (Mar 31 2020 at 18:31):really though i was under the impression that gc pauses were the primary limiting factor in most applications where java wouldnt be applicable
sarahzrf (Mar 31 2020 at 18:31):ewww
sarahzrf (Mar 31 2020 at 18:32):stop using c++
Ben Steffan (Mar 31 2020 at 18:32):I'm not using C++ lol
sarahzrf (Mar 31 2020 at 18:32):then why is your perspective compared to it
Ben Steffan (Mar 31 2020 at 18:32):Because I used it for about 6 years
Ben Steffan (Mar 31 2020 at 18:32):It's by far the language I know the best, too
sarahzrf (Mar 31 2020 at 18:32):im so sorry
Ben Steffan (Mar 31 2020 at 18:33):/shrug
Ben Steffan (Mar 31 2020 at 18:33):Well the upside is that it definitely taught me that software development is fucked
sarahzrf (Mar 31 2020 at 18:33):haha yes
sarahzrf (Mar 31 2020 at 18:33):...c++ is the only popular mainstream language ive deliberately avoided learning
sarahzrf (Mar 31 2020 at 18:34):(php probably deserves it even more but i was younger and dumber when i learned php)
Ben Steffan (Mar 31 2020 at 18:34):Sad actually because you could have a lot of fun with C++
Ben Steffan (Mar 31 2020 at 18:35):It's probably the most cursed language that exists
sarahzrf (Mar 31 2020 at 18:35):/me glances at malbolge
Ben Steffan (Mar 31 2020 at 18:35):lol malbolge is cute
Ben Steffan (Mar 31 2020 at 18:36):malbolge is what you get if you really try to be evil
sarahzrf (Mar 31 2020 at 18:36):u know what ur right
Ben Steffan (Mar 31 2020 at 18:36):C++ is what you get when you get a bunch of people together and try to make something good
Ben Steffan (Mar 31 2020 at 18:36):(and also base it off of C)
sarahzrf (Mar 31 2020 at 18:36):nah when i wanna have a lot of fun with a cursed language i just write some ruby
sarahzrf (Mar 31 2020 at 18:36):or maybe C
Ben Steffan (Mar 31 2020 at 18:36):yikes
sarahzrf (Mar 31 2020 at 18:36):between ruby and C i think i ahve enough cursedness in my life
sarahzrf (Mar 31 2020 at 18:37):i do not need those depths that c++ has
sarahzrf (Mar 31 2020 at 18:38):coq gives me enough yaks to shave
sarahzrf (Mar 31 2020 at 18:40):actually fuck i wonder how cursed coq is compared to c++
Ben Steffan (Mar 31 2020 at 18:41):Pretty sure it's like a little child
sarahzrf (Mar 31 2020 at 18:41):i mean i doubt it beats it but
Ben Steffan (Mar 31 2020 at 18:41):Like, C++ is seriously fucked
sarahzrf (Mar 31 2020 at 18:41):it's pretty fucking cursed
sarahzrf (Mar 31 2020 at 18:41):i just wonder whether it's, idk, to the 50% point
sarahzrf (Mar 31 2020 at 18:41):dont worry, i have heard Things about c++
sarahzrf (Mar 31 2020 at 18:42):i have a pretty decent sense of how cursed it is, i think
sarahzrf (Mar 31 2020 at 18:42):here, look, do you know haskell?
Ben Steffan (Mar 31 2020 at 18:44):I dabble in Haskell
sarahzrf (Mar 31 2020 at 18:44):ok, so you know about typeclasses
sarahzrf (Mar 31 2020 at 18:44):coq has "typeclasses"
Ben Steffan (Mar 31 2020 at 18:44):Yep
sarahzrf (Mar 31 2020 at 18:44):the way they work is
Stelios Tsampas (Mar 31 2020 at 18:44):OK, I am half-way in the presentation and indeed, it's been very, very simple so far. Two things in mind as to why this kind of content has made it in POPL: 1. Many of the more senior members of the audience should not know about that stuff and 2. Oracle is a silver sponsor.
sarahzrf (Mar 31 2020 at 18:44):uh
sarahzrf (Mar 31 2020 at 18:45):so ordinarily coq has an implicit arguments mechanism for arguments like types, where if u mark an argument as implicit, instead of actually supplying it when you apply the function, it gets inserted implicitly by figuring out what it would have to be for the term to be well-typed
sarahzrf (Mar 31 2020 at 18:45):for example
sarahzrf (Mar 31 2020 at 18:46):Definition id (A : Type) (x : A) : A := x. Definition id' {A : Type} (x : A) : A := x.
sarahzrf (Mar 31 2020 at 18:46):the curlies indicate an implicit argument
sarahzrf (Mar 31 2020 at 18:46):you'd write id nat 3 or id' 3
sarahzrf (Mar 31 2020 at 18:46):the latter gets expanded to an application of id' to both nat and 3, which is inferrable because the first arg has to be the type of the 2nd arg
sarahzrf (Mar 31 2020 at 18:47):this makes polymorphic functions usable
sarahzrf (Mar 31 2020 at 18:47):now:
sarahzrf (Mar 31 2020 at 18:47):the way typeclasses work is
sarahzrf (Mar 31 2020 at 18:48):if a particular qualified identifier is registered as "being a typeclass", then you can mark arguments whose type is an application of that identifier as being implicit and inferred by the typeclass mechanism
Stelios Tsampas (Mar 31 2020 at 18:48):Apart from that, and I really have to try to "pick" the lessons from this presentation so far as it not rich in insights, this is a very good example on the gulf between academic "security" and security in the industry. Having worked in exploit. dev./vuln. research labs I can tell you, cognitive load is a thing. And no, people can't just stop using C and switch to dependently typed languages.
Stelios Tsampas (Mar 31 2020 at 18:49):...even with type inference :/.
sarahzrf (Mar 31 2020 at 18:49):and the typeclass mechanism's inference? well, it's actually one of coq's proof search systems, repurposed
sarahzrf (Mar 31 2020 at 18:50):coq has this proof search system based on having a "hint database" and it can try to prove a goal using the lemmas and other kinds of hint in the database
sarahzrf (Mar 31 2020 at 18:50):and they repurposed it to automatically locate terms to fill in arguments
Stelios Tsampas (Mar 31 2020 at 18:50):(go on, I'll continue later, I'll try not to interrupt the flow).
sarahzrf (Mar 31 2020 at 18:50):as "typeclass instance selection"
sarahzrf (Mar 31 2020 at 18:50):it's insane
Ben Steffan (Mar 31 2020 at 18:51):Is it?
Ben Steffan (Mar 31 2020 at 18:51):Why?
sarahzrf (Mar 31 2020 at 18:51):well, it's sort of insane
sarahzrf (Mar 31 2020 at 18:51):it's not insane insofar as it's useful
sarahzrf (Mar 31 2020 at 18:51):but it's fucking cursed
sarahzrf (Mar 31 2020 at 18:52):like
sarahzrf (Mar 31 2020 at 18:52):you get zero of the guarantees that a system like haskell's normally gives you
sarahzrf (Mar 31 2020 at 18:52):haskell has all this stuff about coherence, where there's supposed to be at most one instance of a given signature
sarahzrf (Mar 31 2020 at 18:53):and superclass constraints being smaller or whatever, so that instance search is decidable
sarahzrf (Mar 31 2020 at 18:53):and you can mangle those guarantees with various ghc extensions if you want, but
sarahzrf (Mar 31 2020 at 18:53):in coq, none of that is there to begin with
sarahzrf (Mar 31 2020 at 18:54):you can have 10 different instances of Ord nat and which one gets picked depends on priority annotations or what order they were registered
Ben Steffan (Mar 31 2020 at 18:54):Oh, ok
Ben Steffan (Mar 31 2020 at 18:54):That's... horrible
sarahzrf (Mar 31 2020 at 18:54):and typeclass instances are just proof search hints
sarahzrf (Mar 31 2020 at 18:55):so if you fuck up, you can totally make a system of instances which leads to nonterminating proof search
sarahzrf (Mar 31 2020 at 18:55):and trying to typecheck your term hangs because filling in the instance never finishes
Stelios Tsampas (Mar 31 2020 at 18:55):sarahzrf said:
so if you fuck up, you can totally make a system of instances which leads to nonterminating proof search
Hah! Serves them right!
Ben Steffan (Mar 31 2020 at 18:55):Ah, I mean, if that's the worst that can happen
Ben Steffan (Mar 31 2020 at 18:56):The metaprogramming mechanism of C++ is inherentely Turing complete, and type computations not terminating is, like, Monday
sarahzrf (Mar 31 2020 at 18:56):oh sure
Ben Steffan (Mar 31 2020 at 18:56):Okay, not strictly true because most compilers actually limit the depth of type level computations
sarahzrf (Mar 31 2020 at 18:56):other cursed things: you have full access to the instances hint database as an ordinary hint database, and coq's proof search tool supports hints of various kinds besides just lemmas for application
sarahzrf (Mar 31 2020 at 18:57):so you can just
sarahzrf (Mar 31 2020 at 18:57):extend the instance selection mechanism
sarahzrf (Mar 31 2020 at 18:57):there's a thing called Hint Extern which lets you add an arbitrary tactic to apply to the goal if it matches a certain condition
sarahzrf (Mar 31 2020 at 18:57):so you can add a Hint Extern to the instances database
sarahzrf (Mar 31 2020 at 18:58):and then when coq tries to search for an instance for a particular class, it'll just, invoke your arbitrary tactic
sarahzrf (Mar 31 2020 at 18:58):which can be any, yes, turing complete computation you like
sarahzrf (Mar 31 2020 at 18:58):in ltac, the tactic language, which is itself absurdly cursed
sarahzrf (Mar 31 2020 at 18:59):bbl
sarahzrf (Mar 31 2020 at 18:59):oh god dammit this has been the topic in #category theory not the one in #off-topic :face_palm:
Ben Steffan (Mar 31 2020 at 18:59):whoops
Stelios Tsampas (Mar 31 2020 at 19:49):OK, I finished the presentation and here's my two cents.
It is easy to bash this presentation. How can you present annotations or sanitization libraries as "secure" in front of that audience, people that dabble heavily in dependently typed programming and whatnot, and keep a straight face while doing so. Or show elementary content that's just not what you'd expect in POPL. I don't mean to insult the speaker btw: she is definitely skilled in the field she's in, which is more of the applied type, neither theoretical nor hands-on exploitation.
This presentation is a textbook example of the divide between security industry/research in applied security and security from the TCS/type-theoretic/functional perspective. Functional languages are undoubtedly intrinsically more secure, but the old languages cannot go away. You can't give a crash-course in functional programming and expect people to be productive: functional programming is significantly harder to get into, not least because most beginner PL courses focuse on imperative languages. Also, progress in security is done slowly, causes as few perturbations as possible (otherwise it would seriously hurt productivity), it is heavily guided by the so-called "security arms race" and since there's always pressure for short-term gratification, most solutions are heuristics.
sarahzrf (Mar 31 2020 at 20:17):@Stelios Tsampas i have a reply, but im gonna make it in the topic over in #off-topic , so u shd go check there
Tim Hosgood (Apr 01 2020 at 02:26):sarahzrf said:
nah when i wanna have a lot of fun with a cursed language i just write some ruby
what's cursed about ruby? i was a big ruby fan a few years back (but have never really revisited it with a "formal" eye)
sarahzrf (Apr 01 2020 at 02:42):# will this print 3 or 4? def foo 3 end foo = 4 p foo
sarahzrf (Apr 01 2020 at 02:44):# explain what the following program outputs. def foo(*args) [1, 2, 3, 4, 5] end p(foo[1]) p(foo [1])
sarahzrf (Apr 01 2020 at 02:44):first things to quickly occur to me, i could probably keep going at a steady pace for a while
sarahzrf (Apr 01 2020 at 02:46):i enjoy ruby, but in the same way that i enjoy, like, junk food
sarahzrf (Apr 01 2020 at 02:47):god DAMMIT this is the topic in #category theory again :scream:
sarahzrf (Apr 01 2020 at 02:47):is there some way to lock it