thebadcode

A foolish consistency is the hobgoblin of little minds.

Am I the only one who wishes they had more routine and consistency in my life? People rant all the time about how routine kills creativity and is the last resort of the simple-minded, but it would be really nice to have a little more routine in my life. Wake up at the same time, get a bagel, read the paper, take a shower, drive to work…

Every day I feel pressured to spend my time as efficiently as possible, so it’s hard to sit down and enjoy breakfast or a cup of coffee when you feel guilty about not getting something more productive done. Every morning I wake up and have to decide if I have time for breakfast, time for a leisurely breakfast, or time to shotgun a Red Bull on the way to work. I don’t want to wake up every morning and worry about things that should be automatic like that.

This week I’m switching over to to my new schedule at work (Sun-Wed, 1400-0000), so I’m trying to start something a little closer to a morning routine to go with it. Wake up, write my morning pages, go for a run, get some breakfast, then sit down and hack on some personal projects until it’s time to catch the caltrain. My goal is to stick with this for at least a month and see what happens. I’m hoping this will help regulate my sleep schedule, so that I fall asleep as soon as I get in bed and wake up as soon as my alarm goes off. With any luck, that will help keep me alert and focused all day long so I can finish all my work in just a few days.

Anyone else have this problem, of finding it hard to settle into a routine? If not, what’s your routine look like, and how well has it served you?

Nice quote from Craig Barrett, CEO of Intel:

You tend to find that the older you get, the more conservative you get typically and you kinda start to worry about Moore’s Law not happening. But if you bring the bright young talent and say, ‘Hey, bright young talent, we old guys made Moore’s Law happen for 40 years, don’t screw it up,’ they’re smart enough to figure it out.

Is there anyone who doesn’t think this sounds like a cool idea:

We provide infrastructure and collaboration opportunities for people interested in programming, hardware hacking, physics, chemistry, mathematics, photography, security, robotics, all kinds of art, and, of course, technology. Through talks, workshops, and projects we encourage knowledge exchange, learning, and mentoring.

As a space for artistic collaboration and experimentation, we are open to all types of art - with a special emphasis on the crossover of art and technology. From hardware labs to electronics, cooking, photography, and sound labs, anything that’s creative is welcome.

I hung out with these guys last night for Machine Learning Wednesdays as part of my crash project to prepare for my Google interview. Didn’t learn much that was new, but met a bunch of really cool geeks. I’m actually hanging out at Noisebridge right now, making extensive use of their tech library for the same purpose

The real story, though, is how I managed to get through my undergrad degree in Pittsburgh without ever finding a group like this. Is the hacker culture dead in Pittsburgh, or was I just not talking to the right people? What are other people’s experiences? Anyone in Pittsburgh know of a setup like this that stayed below my radar for four years?

For now, I’m just going to post this without comment, because I don’t want to go to bed while foaming at the mouth.

I had made my demands known and was keeping count.  When 60 days passed without me having a real orgasm (ladies you know the difference), I decided he had been given fair notice and that this was no way to go through my twenties.  I packed his cuff-links and sent him to live on his buddy’s couch.  Fortunately, I had the Bar to focus on and no mental room left to lament the demise of my relationship.  I took the Bar, drank myself into oblivion, and headed to South America for a much needed vacation.

Yeah, yeah, I started playing World of Warcraft, bite me. If you find yourself on Arthas, look me up. My character name is Bahdqode

Words of wisdom from Steve Yegge on MT code:

So when safe alternatives to existing unsafe technologies come along, it takes about ten to fifteen years before everyone’s switched over. Not that the unsafe users actually switch; that’s just how long, on average, it takes the majority of them to be killed accidentally by their product, leaving only the new, safer programmers behind.

01:11:14 PM) ian: see also wtf notation: http://www.andrew.cmu.edu/user/iev/alt.pdf
(01:12:01 PM) austin: what am i looking at?
(01:12:36 PM) ian: an almost-correct proof of the WFF of chruch’s first order logic on line 100
(01:12:44 PM) ian: that has been eating my soul for like two days
(01:13:04 PM) ian: more math goes between lines 20 and 90
(01:16:17 PM) austin: *church?
(01:16:32 PM) ian: yes.
(01:16:58 PM) austin: im not sure i understand what you’re trying to prove
(01:17:20 PM) ian: you see that huge well formed formula on line 100?
(01:17:54 PM) austin: yes
(01:18:06 PM) ian: i’m trying to prove that it’s a theorem of first order logic
(01:18:19 PM) ian: like for any predicate constants S, D, and F of that form, that statement is true
(01:18:40 PM) austin: i gotcha
(01:18:52 PM) ian: so you work it backwards by first noticing that it’s of the form A -> B. so, like always, you’re like “well A->B iff by assuming A i can derive B”
(01:18:56 PM) ian: and then you go to twon
(01:18:58 PM) ian: *town
(01:19:23 PM) austin: so more like “an almost-correct proof that the the wff on line 100 is true under fol”
(01:20:07 PM) austin: right?
(01:21:56 PM) ian: yeah. i mean it’s sort of assumed that this is all FOL and that you’ve set a certain syntax
(01:22:11 PM) austin: i gotcha
(01:22:32 PM) austin: i cant decide if that sounds like more or less fun than the javascript templating engine im working on
(01:22:40 PM) ian: haha
(01:22:49 PM) ian: so this particular WFF is preposterous and retarded
(01:23:06 PM) ian: cause no human would ever think of something with that many quantified variables
(01:23:11 PM) ian: we just don’t have intutition in that many dimensions
(01:23:14 PM) ian: so it’s pure syntax
(01:23:31 PM) austin: ugh
(01:24:17 PM) ian: yeah
(01:24:26 PM) ian: here lemme show you something that’s borderline meaningful.
(01:24:29 PM) ian: borderline
(01:27:02 PM) ian: http://andrew.cmu.edu/~iev/x2119.pdf
(01:29:10 PM) ian: there’s *almost* actual beauty there, cause you start from a very common tautology and get something odd looking
(01:29:17 PM) ian: and it’s 14 lines
(01:31:13 PM) austin: im trying to parse your syntax
(01:31:27 PM) austin: are you using the subset inclusion for implication?
(01:31:32 PM) ian: oh. yeah.
(01:31:41 PM) ian: there’s a good reason for that
(01:31:43 PM) austin: and dot for “such that”
(01:32:10 PM) ian: dot is an omitted [ where its mate goes as far to the right as it can without fucking your shit up
(01:32:18 PM) austin: 0.o
(01:32:33 PM) austin: that sounds an awful lot like python using whitespace for indentation
(01:32:36 PM) ian: this is a VERY archaic notation that my prof uses; note that this pdf is generated by lisp that pfenning wrote in the 80s
(01:32:50 PM) austin: wowsers
(01:32:53 PM) ian: yeah
(01:33:09 PM) ian: the system is called ETPS; it was pfennings PhD thesis
(01:33:48 PM) ian: the reason that you want to use \supset instead of \implies is that it leaves your names space less ambiguous when you want to prove theorems in informal mathematics about the formal system
(01:34:02 PM) austin: bwahaahaha
(01:34:05 PM) ian: so if you don't allow \implies in the object language, you can use it freely in the metalanguage
(01:34:28 PM) ian: otherwise you'd have to subscript your implies or paint some of them green or something
(01:34:51 PM) austin: and to match up the statements on the right... so for example "choose y 52" means "bind y to some value that makes statement 52 evaluate to true"
(01:35:08 PM) ian: you should reload the pdf actually, with less retarded line numbers.
(01:36:32 PM) ian: you can think of saying "choose y" as instantiating an existential quantifier. it's called rulec and there are 23523523 technical restrictions on it, but oyu're basically going "well i know that there is some x for which this thing is true, and i haven't called anything else y yet, so i'm going to assume that that x that makes this shit true is actually called y"
(01:36:54 PM) austin: right
(01:37:04 PM) austin: is that different from what i said in some important way?
(01:37:13 PM) ian: yes
(01:37:20 PM) ian:
(01:37:52 PM) ian: "bind" and "make it true" is a bad way to think about it; you know it's true for something, so you're choosing to call that something y
(01:39:08 PM) austin: im thinking about from a comp and incompleteness perspective, where everything we did basically involved a brute force search of all the natural numbers for one that had some property we needed
(01:39:11 PM) ian: like .. you can't make things true or false. its too inherent in their nature to be dependent on a particular choice of something
(01:39:49 PM) ian: that is to say, valid statements are valid reguardless of the model that you pick for them
(01:39:55 PM) ian: lolcompleteness
(01:40:02 PM) austin: i see the distinction now
(01:40:05 PM) austin: and yeah, no joke
(01:42:20 PM) austin: it was like "well, we've proved the existence of such a program, but we need to actually produce it, so.... lets start from 0 and count up, treating each natural number as a godel-encoded representation of a set of a statements in a turing-complete langauge, and run each one on our function which is capable of universal computation to see if its the one we're looking for"
(01:42:36 PM) ian: yup
(01:42:42 PM) ian: C&I is a dirty hack
(01:42:56 PM) austin: that course was fun
(01:43:07 PM) austin: it was nice to forget about runtime complexity for a semester
(01:43:20 PM) ian: according to trev, another C&I vet, we covered the whole syllabus in CDM in three lectures
(01:43:25 PM) ian: klaus: not a nice man
(01:44:17 PM) austin: just imagine. boss: "hey, i need you to write a relational database system" programmer: "sure thing, ill just go search the cosmos of pure numbers for one"
(01:44:32 PM) ian: haha. yeah.
(01:44:47 PM) austin: hmmm
(01:45:24 PM) austin: c&i is with whats his name, the quiet logic prof in the phil department, right? not the crazy red-haired bearded dude?
(01:45:36 PM) ian: it's avigad [sic] i think
(01:45:48 PM) austin: yah, i didnt take c&i, i took the *other* one
(01:46:08 PM) ian: oh right sarah was in C&I with trev, not you
(01:46:23 PM) ian: or she was until she dropped it. or she was until i stopped paying attention and then she still was, or something
(01:46:40 PM) austin: yeah, she ate shit and died in c&i
(01:46:52 PM) ian: oops.
(01:47:01 PM) austin: c’est la vie
(01:47:09 PM) ian: yeah
(01:47:19 PM) ian: so do you see how that proof works? cause i think it’s pretty damn cool
(01:47:30 PM) ian: cause just the statement of the theorem makes no-god-damn-sense
(01:49:52 PM) austin: im stuck on statement 54; arent you assuming the existence of an x such that P(x)
(01:50:23 PM) ian: hit refresh?
(01:50:40 PM) ian: i had a copy with moronic line numbers up for like 10 seconds, wherein your browser decided to cache it
(01:51:26 PM) austin: line 10
(01:52:00 PM) ian: so line 10 is true by definition of implication
(01:52:05 PM) ian: on line 9 i had ~Py
(01:52:17 PM) ian: and if you have A, you know that A OR B is true for any B
(01:52:24 PM) ian: so then you have ~Py OR Px
(01:52:30 PM) ian: which is Py IMPLIES Px
(01:52:39 PM) ian: basically, false implies anything
(01:54:09 PM) austin: oh, i read line 9 wrong, i get it
(01:54:37 PM) ian: yeah
(01:54:43 PM) ian: super cool though
(01:55:25 PM) ian: basically the whole thing formalizes the only possible way that (14) could be true. like if P is true for any input, then Py -> Px reguardless of how you get x and y
(01:55:28 PM) ian: cause true implies true
(01:55:45 PM) ian: and if P is false for any one input, we’re choosing to call it y, and then false implies true for anything
(01:55:57 PM) austin: but thats just pedantic noise
(01:56:05 PM) ian: no?
(01:57:06 PM) ian: this is a rigorous proof that for any single input predicate P, i.e. any function from any set to {T,F}, that (line 14) is the case
(01:57:21 PM) ian: well i guess it’s only first order logic
(01:57:30 PM) ian: so it’s from any set that doesnt contain sets
(01:57:55 PM) ian: in the sense taht first order logic quantifiers cannot quantify sets, only individuals
(01:59:22 PM) austin: like, lets define p(n): (n == 0)
(01:59:57 PM) austin: so for all x except for 0, y is unbounded
(01:59:59 PM) ian: okay.
(02:00:22 PM) ian: congratulations, you just swapped the quantifiers!
(02:00:35 PM) austin: i was just going to say, wait i have that backwards
(02:00:36 PM) austin:
(02:00:39 PM) ian: yeah.
(02:00:49 PM) ian: so P(n) := true iff n = 0
(02:00:58 PM) ian: i choose y = 9
(02:01:02 PM) ian: 9 != 0
(02:01:11 PM) ian: so forall x (false implies Px)
(02:01:16 PM) ian: which is true
(02:01:18 PM) austin: right right right
(02:01:34 PM) austin: basically, you either find an interesting positive case, or you rely on the definition of implication
(02:01:39 PM) ian: yah
(02:01:49 PM) austin: which… seems unsatisfying
(02:01:53 PM) ian: haha
(02:02:04 PM) ian: that’s just cause material implication is gayer’n liberace
(02:02:25 PM) austin: because for all practical intents and purposes, you might as well leave off the second part
(02:02:45 PM) austin: and just say “sometimes, single input boolean functions have more than one input that satisfies them”
(02:03:05 PM) ian: so i mean, even the positive case isn’t interesting
(02:03:30 PM) ian: like if you can choose some y such that Py, it must be the case that forall x Px
(02:03:41 PM) ian: so you’re really relying on the definition again, as you put it
(02:04:05 PM) austin: incidentally, am i the only one that doesnt understand the deep wisdom in defining implication that way?
(02:04:21 PM) ian: nope. you should have gone to grad school and taken constructive logic and linear logic
(02:04:27 PM) ian: but you went to california instead
(02:04:29 PM) ian:
(02:04:49 PM) ian: but seriously, material implication is indeed quite odd.
(02:05:12 PM) austin: http://uncyclopedia.wikia.com/wiki/X_windows
(02:05:18 PM) austin: Just as X-Windows reverses the meaning of “feature” and “problem”, it reverses the meanings of “server” and “client” (your screen serves resources to programs, making them the clients. You have to be a very deep geek with amazing powers of contemplation indeed to see why this is obviously and elegantly sensible), “black” and “white”, “up” and “down” and “good idea” and “bad idea.”
(02:05:31 PM) ian: because while it might be true to say that “if two is even, then i’ll go to the party”, it’s not particularly profound
(02:05:39 PM) austin: thats how i always felt about that definition
(02:05:55 PM) ian: in the sense that the parity of two is somewhat irrelevant to your drunkenness later in the day
(02:06:02 PM) austin: not sure if you ever read uncyclopedia btw, but that article is fucking *hysterical*
(02:06:07 PM) ian: but formalizing “relevance” … well. good luck.
(02:06:26 PM) ian: yeah, i <3 the X windows article
(02:07:15 PM) austin: and yeah, i understand that its *true* to say “if 2 is odd, then 3 is even”
(02:08:12 PM) austin: but it seems like it would have been a better idea to handle that case as part of the definition of a wff or something
(02:08:39 PM) ian: heh. wffs aren’t even defined to include implication
(02:08:43 PM) austin: *sigh*
(02:08:49 PM) ian: implication is only a short cut for writing ~A v B
(02:09:30 PM) ian: it’s economical to prove things about a small of WFFs, constructed of a basis vector of connectives
(02:09:53 PM) ian: which is to say, all WFFs can be described in terms of ~ and v, so if you prove shit about that, you’ve proved it about all of them
(02:10:00 PM) ian: (forall is not a connective)
(02:10:08 PM) ian: so why make your induction longer and harder if you don’t have to
(02:10:18 PM) ian: cause really your only tool here is induction on the construction of a WFF
(02:11:43 PM) ian: it’s a mild economic concern if you assume that they method of production of proofs is a human with a pen, but as soon as you try to automate that, one less connective to worry about could be the difference between polynomial and haha-good-luck runtimes
(02:11:48 PM) austin: id rather think of wff’s as a set of strings accepted by a function instead of set of inductive generating rules, but i take your point
(02:12:09 PM) ian: so that’s how you define the set of WFFs, but not how you prove things about them
(02:12:43 PM) ian: the set of WFFs is to be thought of as the intersection of all sets of formulae where if A is in any one of those sets then ~A is as well; etc.
(02:13:04 PM) austin: wait wait wait
(02:13:06 PM) ian: and from that definition, once you have the set of WFFs, you can go out and try to reverse engineer a nice inductive structure
(02:13:13 PM) ian: hehe
(02:13:58 PM) austin: are you saying that the way you do *proofs* in fol is to start with nothing but a set of rules for modifying wff’s and a set of tautologies and then just let ‘er rip?
(02:14:19 PM) ian: hahah
(02:14:19 PM) ian: you wish
(02:14:25 PM) ian: that’d be living life in the high style
(02:14:35 PM) ian: you accidentally assumed that you know what a tautology is
(02:14:49 PM) ian: proofs in FoL are entirely syntactic beasts
(02:14:51 PM) austin: because that sounds an awful lot like a function for iterating over every provable statement in fol
(02:15:00 PM) austin: wait
(02:15:04 PM) austin: im mixing my terms
(02:15:08 PM) ian: and it’s very important to note that they only have semantic value by coincidence
(02:15:27 PM) austin: the wff-edness of a thing has nothing to do with the truth or falsehood of a thing, right?
(02:15:32 PM) ian: yah
(02:15:44 PM) ian: erth
(02:15:44 PM) ian: no
(02:15:47 PM) ian: kind of
(02:15:57 PM) austin: well, in the sense that if something isnt a wff, it cant be true or false at all
(02:16:02 PM) ian: take propositional calculus; FOL without quantifiers
(02:16:15 PM) ian: its’ not all that different than FOL but it’s nicer to talk about in some cases
(02:16:44 PM) ian: you define this beast by defining a formula, and then choosing some set of formulae to be “Well formed”
(02:17:11 PM) ian: if you choose that set carefully, you can prove that every wff that is a theorem, i.e has a proof, is true under a certain system of evaluation, and that every wff that is true has a proof
(02:17:17 PM) ian: i.e. is a theorem
(02:17:18 PM) austin: whoa whoa whoa
(02:17:29 PM) ian: wut.
(02:17:44 PM) austin: “under a certain system of evaluation”
(02:17:56 PM) austin: oh wait, i misread what you said
(02:18:20 PM) austin: i missed the “that” in “ever wff that is a theorem”
(02:18:55 PM) austin: ok, so yes. its possible to generate statements which are wff’s but which are not theorems
(02:19:03 PM) ian: yes. like “Px”
(02:19:05 PM) austin: but not the other way around
(02:19:11 PM) ian: this is well formed. this is not a theorem.
(02:19:27 PM) austin: ok, thats what i thought
(02:20:55 PM) austin: so back to what i was saying, wff is nothing but a stupid syntax game, in the sense that our definition of a wff just *happens* to have semantic meaning under any propositional system you want to work in
(02:21:02 PM) austin: thats what you’re saying, right?
(02:21:26 PM) austin: so i buy into wff being syntax, but not that FOL proofs are mere syntax
(02:21:50 PM) ian: i mean they’re defined that way
(02:22:07 PM) austin: i mean, “true” and “false” arent syntactic concepts
(02:22:39 PM) ian: a proof of first order logic is defined to be a series of wffs, where the last statement is the thing being proved, and each wff is either an axiom or follows from one of the rules of inference from one or more preceeding wffs
(02:22:44 PM) ian: these are syntactic beasts entirely
(02:23:31 PM) ian: the magic/beauty/genius of the thing exists in the proofs (note that these are proofs in the metalanguage, about FOL, not in FOL) of consistency and completeness
(02:23:53 PM) ian: which establish the connection between the syntactic beasts of FOL wffs and proofs and a particular semantic notion
(02:23:58 PM) austin: *a proof IN first order logic?
(02:24:29 PM) ian: ah. yeah. the terms are used interchangable, because you can’t “prove first order logic”
(02:24:38 PM) ian: in the same sense that you can’t “prove a banana”
(02:26:03 PM) austin: thats what i *thought*, but it sounds like you’re proposing that fol is meaningless syntac gibberish until you go through a proof of an isomorphism between fol proofs and “perfect isoceles triangle” proofs
(02:26:30 PM) ian: FOL is meaningless syntactic gibberish
(02:26:39 PM) ian: these pdfs i’m showing you are utterly without semantic value
(02:26:44 PM) ian: deliberately so
(02:26:55 PM) ian: they don’t mean anything whatsoever until you pick a model
(02:27:06 PM) ian: then if you picked your model carefully, hey, you might get something out of it
(02:27:21 PM) ian: that’s the point
(02:27:54 PM) austin: why would you need to pick a model? proofs are proofs. once you have a mapping from fol symbols to meaningful proof semantics, theres nothing left to do
(02:28:10 PM) austin: there is only One True Proof System
(02:28:14 PM) ian: WRONG
(02:28:21 PM) ian: oh dear god don’t say things like that
(02:28:44 PM) ian: the proofs of consistency and completeness are parametrized on the existence of a user chosen model
(02:29:50 PM) austin: i mean, its kind of a philosophical question but a “proof” of something, as in, something you write down on paper, is just the syntactic expression of some higher semantic proofi-ness, which holds regardless of your syntax
(02:30:22 PM) ian: no
(02:31:20 PM) ian: the syntax is the syntax. it’s good syntax because for whatever carefully chosen semantic system you produce, a wff with a syntactic proof will be valid
(02:31:34 PM) austin: thought experiment
(02:31:55 PM) austin: you and i are alien philosophers living on two different worlds which are lightyears apart
(02:32:10 PM) ian: note that i’m probably over stating it when i say “carefully chosen”; there are some important technical restrictions in FOL on the model you choose, i.e. the semantics you choose, but analagous systems exsit for more and more complicated desires
(02:32:29 PM) austin: a third alien species flies down and scoops up your proof that we were just looking at before
(02:32:51 PM) austin: flies over to my planet
(02:33:17 PM) austin: symbolically translates your proof in fol to a proof in whatever whacko banana-proving language i use
(02:33:47 PM) austin: (which is obviously possible; thats nothing but symbol manipulation since we both agree there are no semantics you could fuck up yet)
(02:34:16 PM) austin: they beam your proof into my room, i read it and agree with it
(02:34:28 PM) austin: now, *you and i have not shared any semantic knowledge whatesover*
(02:34:53 PM) austin: there has been *zero* communication between us in any way that you could call meaningful
(02:35:06 PM) austin: but we can *agree* on the semantic meaning of your proof
(02:37:01 PM) austin: which implies the existence of a higher concept of proofi-ness that *must* be shared by *all* syntactic systems for representing proofs
(02:37:54 PM) austin: the various kinds of models you’re talking about are really just subsets, right?
(02:38:18 PM) ian: we can only agree on that by applying either the consistency or completeness theorems
(02:38:26 PM) austin: as in, “some models arent powerful enough to represent this statement, which IS true in some other more powerful model”
(02:38:41 PM) ian: until then, we can only agree that the proof is a correct application of the syntactic judgements defined by my FOL or your isomorphic banana-FOL
(02:42:05 PM) austin: but the incompleteness theorems can only be applied to syntactical systems for *expressing* proofs
(02:43:00 PM) ian: erhm. gödel proved both his famous incompleteness theorem, and a completeness theorem of FOL
(02:43:15 PM) ian: which are both correct and not as contradictory as they sound like they ought to be
(02:44:39 PM) austin: yes, i know. FOL is complete but not consistent, and as an encore the incompleteness theorem shows that no proof system can be both
(02:45:10 PM) ian: FOL is both complete and consistent, but not decidable
(02:46:06 PM) ian: so wff is a theorem iff wff is valid under every interpretation
(02:46:10 PM) ian: but good luck finding proofs, chump
(02:47:04 PM) austin: er, but your original claim was that FOL is nothing but syntactic wankery, right?
(02:47:30 PM) ian: no.. my claim is that proofs executed in the frame work are syntax only
(02:48:42 PM) austin: and my claim is that while proofs executed in the framework are syntax only, it isnt just a coincidence that we can impose a model that creates semantic meaning
(02:50:17 PM) austin: and that further, EVERY such syntactic system is nothing but the shadow of some fundamental semantic structure
(02:52:27 PM) ian: in the sense that we define semantic structures in a feeble attempt to mimic the way we perceive the world, and that we’re too influenced by that perception to be pleased by syntax too far away from it—maybe
(02:53:14 PM) ian: but there are syntactic systems which are mathematically both complete and consistent and are lightyears away from being “nice”
(02:53:31 PM) ian: highlighting the flaws in the notions of consistency and completeness
(02:54:06 PM) austin: but that goes back to my thought experiment. regardless of the feebleness of *our* bogus perceptions and syntactic models, a underlying semantic reality has to exist
(02:54:21 PM) ian: no
(02:54:34 PM) ian: that’s raw theology
(02:54:46 PM) ian: you can say “there is a god instead of “there is an underlying semantic reality”
(02:57:07 PM) austin: you have to accept that two mathematicians trading proofs are either:
(02:58:18 PM) austin: 1) trading syntax which would be meaningless without an underlying shared semantic reality
(02:58:52 PM) austin: 2) trading their *particular* semantic realities
(02:59:41 PM) austin: which may not have any overlap at all except through coincidence, and *certainly* dont have anything to do with the “real world”, for whatever “real” even means
(03:01:13 PM) austin: which is very similar to 3), which is that they arent sharing semantics at all, and that its a staggering coincidence/miracle/mass delusion that mathematics ever seems to get done at all
(03:02:47 PM) austin: fuck. in *my* semantic reality, i have to give a demo in an hour.
(03:03:12 PM) ian: haha.
(03:03:14 PM) ian: owned

It’s a mirage! I’m trying to tell y’all, this is SABOTAGE!

Happy Halloween, everyone! More Halloween coming, as they happen.

I had this conversation with a friend, and realized that it was a pretty decent analogy:

(09:03:10 PM) austin: imagine that i built this amazing air filter to wear over your head
(09:03:26 PM) austin: it will protect you from all possible harmful viruses, pollution, bacteria, whatever
(09:03:43 PM) caroline: uh huh
(09:04:30 PM) austin: but it covers your entire head and vaccuum seals to your neck
(09:04:53 PM) austin: and my filter material isnt transparent, so you cant see through it
(09:05:09 PM) caroline: eep!
(09:05:11 PM) caroline: no good!
(09:05:37 PM) austin: so you have two little latches that open the filter up in front of your eyes so you can see out
(09:06:09 PM) caroline: k
(09:06:26 PM) austin: so now you say to me “this is totally worthless; i cant do anything without opening these stupid latches in front of my face, and once i open them, i may as well not even be wearing this stupid thing”
(09:06:52 PM) austin: and my response is “no, you just arent using it right! no one ever told me you needed to be able to see AND be protected from bad things simultaneously!”
(09:07:17 PM) caroline: haha!