Thread by @deontologistics

@meier_kreis @eripsa @texturaaberta I can’t say I’ve read both of these through, but they’re good reference texts with exercises and such if that’s your thing. The first has an intro to set theory and meta logic toward the end, the second builds up from recursive function and Turing machines to Godel’s proofs.

@meier_kreis @eripsa @texturaaberta To be quite honest, most of my maths knowledge comes from spending too much time on nLab, which means I’ve got a much better grip on high level relations between fields and concepts than on practical techniques for proving things. Still, this can be philosophically useful.

@meier_kreis @eripsa @texturaaberta Beyond this, ArXiv is a veritable treasure trove of papers on maths and computer science. In fact, there are a lot of great papers (and even courses) that can be found free online with a quick google. The academic norms about such things are so much better.

@meier_kreis @eripsa @texturaaberta However, if you want a conceptual guide that can structure your googling, I recommend beginning with the SEP article on the Church-Turing thesis: plato.stanford.edu/entries/church…

@meier_kreis @eripsa @texturaaberta The key thing to get one’s head around is the equivalence between different models of computation, and the more general fields/systems they’re situated in, principally: recursive functions, Turing machines (automata theory), and lambda calculus (term rewriting systems).

@meier_kreis @eripsa @texturaaberta This gives you the basic formal and conceptual purchase on the two ways we usually think about computation, namely, in terms of machines, and in terms of languages. Exemplars of these perspectives in CS are Scott Aaronson and Robert Harper.

@meier_kreis @eripsa @texturaaberta If you want to understand the Curry-Howard(-Lambek) correspondence and how that forms the basis for things like HoTT, then Harper’s lectures are great. If you want to understand the relation between computability theory and computational complexity theory, Aaronson is your guy.

@meier_kreis @eripsa @texturaaberta In particular, this paper by Aaronson should leave you awash in ideas: scottaaronson.com/papers/philos.…

@meier_kreis @eripsa @texturaaberta The other person I will mention here is Samson Abramsky, who is a complete all-rounder and philosophically deep thinker on the question of what computation (and information) is, and the challenges the field still faces: arxiv.org/abs/1604.02603

@meier_kreis @eripsa @texturaaberta His distinction between computations in which *what* is computed is important (i.e., batch programs) and those in which *how* they behave is important (i.e., online systems) is extremely important, and often not sufficiently appreciated by people who apply CS in other fields.

@meier_kreis @eripsa @texturaaberta That should also give you a taste of the difficulties posed by concurrent computation, which is a topic with some deep philosophical subtleties and no unitary formal description. It's often not explained well, nor is the difference between it and parallel computation.

@meier_kreis @eripsa @texturaaberta One way to get a feel for it is to look at the dominant machine model of concurrent computation(analogous to TMs): Hewitt's actor model (en.wikipedia.org/wiki/Actor_mod…). Beware, Hewitt can get a little cranky around the edges, but there's something philosophically significant in there.

@meier_kreis @eripsa @texturaaberta In particular, this will force you to get a grip on the difference between stateless and essentially stateful computation. The former is principally the province of languages and the latter the province of machines.

@meier_kreis @eripsa @texturaaberta It also might introduce you to the idea of non-deterministic computation, which is another significant distinction best thought about from the machine side, i.e., automata theory.

@meier_kreis @eripsa @texturaaberta Coming at the topic from logic, you'll no doubt be much more inclined towards the language perspective, because it's there that logic becomes useful in articulating type theories that guarantee programs will behave well if they are written well. The domain of CH correspondences.

@meier_kreis @eripsa @texturaaberta Wadler gives a good overview of the current range of CH correspondences and what they mean: homepages.inf.ed.ac.uk/wadler/papers/…

@meier_kreis @eripsa @texturaaberta Crucially, these involve a range of term-rewriting systems beyond typed lambda calculi. I personally hate these things, as I find the syntax a nightmare to read, but you can get a grip on the concepts without mastering the methods.

@meier_kreis @eripsa @texturaaberta However, there are a range of connections between logics and machines that get exploited in formal verification. The Abramsky paper talks about some (such as dynamic logic), but this paper also gives a great historical overview of the field: homepages.inf.ed.ac.uk/wadler/papers/…

@meier_kreis @eripsa @texturaaberta I think that's everything for now. Maybe a little overkill, but there'll be something in there you find useful. The other thing to do here is do some programming, if you don't already. This is one step I've struggled to take myself, beyond playing with a bit of Haskell.

@meier_kreis @eripsa @texturaaberta Oh, and no such list would be complete without me including my favourite paper, Martin-Lof's positively crystalline paper explaining that mathematics is synthetic a priori using type theory: archive-pml.github.io/martin-lof/pdf…