On Free Will and AI: A Rant and/or Rave

Free will. I know that its existence and nature has been debated to death, but given the prevalence of pop-science articles about AI and whether evil super-intelligences will spell the doom of humanity it’s a topic I want to ramble about for a bit.

First off, we need to define what we mean by “free will”. I think the easiest definition is that to have free will means to have the ability to make a deliberate choice between alternatives. If you haven’t spent many insomnia laden nights worrying about this topic, you might be wondering “okay, that sounds good, why is that controversial?”. Fundamentally, the issue is that physics as we understand it doesn’t leave a lot of room for “choice”. In the classical, Newtonian, view of things the motion of every particle is deterministic. Once you have the initial conditions, you can turn-the-crank on the equations of motion and get the position and momentum of every particle in the universe at any point in the future. Thus in classical mechanics, there can’t be any ability to make a choice since everything that happens follows exactly from everything that happened before it.

Now, folks sometimes try to dig into quantum mechanics hoping that it will save us and provide a clue as to how consciousness and choice work. The problem there is that probabilistic physics doesn’t allow choice any more than deterministic physics. There is still no reflective mechanism that allows for a conscious entity to deliberate and choose.

Do we then conclude that free will is an illusion? I don’t think so. I believe we have free will. I think we have the ability to make choices. In part, because a world where we

  • seem to make choices
  • can debate on our ability to make choices
  • are able to think we make choices
  • but don’t actually make choices

seems very, very unlikely. Of course, if I’m wrong then I don’t suppose I have any choice in my beliefs anyway (1). I’m not even necessarily appealing to a supernatural cause for free will. My best guess is that there’s something deeply strange about the universe that we have yet to discover. But who really knows? I certainly don’t. For the rest of this piece, though, I will be assuming that free will somehow exists.

Where does this fit in with AI, though? It’s a long standing anxiety in science fiction that machines will be sapient just like us and rise up to destroy us, and it’s an anxiety that’s finding its way into tech journalism as AI become more and more prevalent and powerful, but is it even possible? I’d argue that we don’t know whether a machine can ever be conscious. If my assumption is correct and we do have free will, then I imagine we’ll need to understand how this choice works physically before we can make a machine that use it. There’s a few potential showstoppers here. We might not find a physical mechanism for free will. Even if we find one, it’s not obvious to me that it would be easily harnessed in a computer-as-we-know-it. As much as I’d love for them to exist, I don’t particularly see sentient machines happening in the near future.

We can’t talk about thinking machines without discussing the Turing test. The Turing test doesn’t make any reference to free will or choice as a requirement for being a thinking machine, just the ability to fool a person 70% of the time after a five minute conversation into thinking they’re speaking with a human. I think that Turing’s test isn’t necessarily helpful given our current computational power. What I mean is that I agree with the extensional point of view that if a machine isn’t distinguishable in behavior from a person, then there’s no useful distinction made between the machine and us, thus it’s completely reasonable to call the machine “thinking”. I also believe that Turing didn’t realize how quickly our computational power and storage size would grow. Chatbots have become fairly common place at this point, but the facade is rather thin. Even if the program is capable—with enough AIML rules, processing power, and clever heuristics—of convincing a person that they are speaking with another human being in the short term, it doesn’t tell us anything about the ability to make choices.

If our AI cannot make deliberate decisions, then should we be concerned then with AI-as-we-know-it running out of control? I don’t think so, at least not any more concerned than we should be about any large and important software system. This may seem like a facile point, but without choice there’s no room for AI to surprise us if we’ve properly proved properties of their behavior. If anything, I think this is just a strong argument that we need to invest further in careful program construction and better theorem proving and formal methods technologies so that we no longer have to pay an overhead of many person-years to analyze a large system.

(1) I’m being facetious, but I thought it would be too much of a digression to discuss compatiblist views of free will with determinism. It’s probably obvious that I disagree with them, but I’m not dismissive of them.

I actually want to talk about a video game today: TIS-100. It’s not terribly new, but it’s new to me and I don’t remember seeing people talk about it very often.

I had never imagined programming puzzle game could be a genre, but now I want dozens of games like this because of how much fun it’s been.

It’s a great puzzle game because it’s programming assembly for a vaguely made up architecture of independent communicating nodes that are, for the sake of the puzzle, very limited in their features*. Each node can hold only a small number of instructions and has channels to communicate with its geometric neighbors, channels which block on empty reads or full writes. Each node has two “registers” that can hold an integer and there’s basic instructions for register manipulation and one of the registers is specially used for the control flow constructs and arithmetic instructions. It’s a very simple but very cute architecture.

I’m not done with the game, being almost halfway through with all the puzzles (unless more become available that don’t have a placeholder?), but it’s generally been a lot of fun. The puzzles are well-designed in that, at least so far, each one has had a particular programming concept that you’ve needed to internalize to finish it and the lessons have built on each other in a logical progression.

In fact, I’m enjoying this so much I’ve started a little project on github where I’m working on a simulation of similar kind of hardware. My goal is to eventually compile higher level languages down to a configuration of programmed nodes. The main difference is that I’ve removed the instruction limit because I feel like it was largely there for the puzzle factor. The intermmediate goal is to have a slightly-higher-level language that is basically an abstracted version of the assembly code for individual nodes where rather than geometry there’s just a general notion of naming entities in your file and letting them communicate, then with a little graph munging it can either be compiled down to a solution of connected nodes or throw an error that it would require a non-planar graph. That’s at least my current thought, we’ll see when I get around to actually trying it.

*Honestly, it reminds me a lot of how I’ve heard folks describe data flow in gpus for general programming, but I know so little about that topic that I don’t know if that’s an accurate assessment.

A New Year

So my medical leave is done, I’m getting back to grad school, and it’s the start of a new year.

It was a really good year, for me. I got a lot of rest. My health improved. I’ve even been medicating my mental illness more, which in the past few months means that I’ve obtained a rather healthy github streak (115 days and counting at the time of writing). I spent a few months curriculum writing for a code school. I’ve made progress on several long-term writing projects, including a book of essays and an intro-to-computer-science book as well as picking away a little bit on my “working while mentally ill” project, and I’ve managed to work on a lot of little side projects, including my rough sketches about what a true privacy oriented social network should look like.

I also finally gave a talk at the Open Source Bridge conference and got a magazine article published, both of which were about explaining the fascinating mathematical limits, and open questions, of computation to a general audience. There’s a lot of pragmatic, useful things that are good to know: that computation exists abstracted away from the particular of any implementation, that there are hard theoretical limits to what a program can do, etc. But one of the completely impractical things I love to bring up is that the relationship between computability and physics has some very weird and fascinating implications for 3D printing. Essentially, if the laws of physics aren’t computable, then there are clear limits to the complexity of a thing that can be constructed in a 3D printer. If the laws of physics are computable, however, then in principle 3D printing has no limits beyond physics itself: any physical system could be created programmatically. Now, this is possibly of more interest for science fiction than engineering any time in the next century, but it’s engaging nonetheless.

One of the big things that happened over this medical leave was realizing just how bad off I had been before. I could fake functionality for brief periods, but often I was having trouble with reading and listening comprehension and with keeping anything in my head for more than a few seconds. A couple of months into this year off I realized that (shock, gasp) I could actually concentrate. I could sit down with a book and read without having to reread the same sentence five times to actually digest it. I could work on something for an hour or so and actually think about it. I could even work on something for several days in a row without forgetting everything I’d been thinking about in the first place. I’ve been wrung out and ill for practically my entire life, so this whole “I can function like a healthy person” thing has just been a revelation. Medicating my panic and my “reality and I aren’t on speaking terms” days has contributed significantly to this discovery. My worst mental health episodes now last for maybe an hour or two at a time instead of days or weeks of being unable to function. It’s still not fun, mind you, but at least I don’t feel like I’m a bad dice-roll away from losing a month or two of my life at any given moment. It’s just a major improvement to be able to have a bad evening or a bad day instead of a bad [arbitray length of time].

The next two terms are going to be incredibly busy. I’m both getting back to teaching courses and actually giving my thesis proposal. I’m not going to lie, I’m probably way more terrified of my thesis proposal than I need to be for someone who already has a clear outline of (1) what I’ve already done (2) what I want to do (3) how I’m going to do it and (4) how it contributes to my field. I keep feeling like I practically need to have my dissertation done before I even give my proposal. Part of making my proposal this spring is that I’m actually rebuilding some of my old unpublished work on higher dimensional type theory (now that I can do something about the panic attacks it can give me). I already started doing that this last month and it’s been going great. I think I’m actually going to get these papers out there, finally finally finally. This is work I haven’t been able to touch in over three years because I was working on it around the time I was assaulted in 2012, the last real time I was productive until this year off. The panic attacks have come every time I’ve tried to reconstruct all of it because it pushes bad buttons associated with how suicidal and scared and messed up I was at that time, because brains are stupid.

In regards to this blog, I’m going to try and have a Tue/Thu publishing schedule. I’m going to avoid making the same mistakes as before and just publish something on my scheduled days, even if it’s not as in-depth as I’d like. To that end, by the time this post is published I’ve already built up a bit of a buffer in case I have some extra busy weeks.

Virtues and Type Theory

So for today I thought I’d write a short post reviewing the paper The Seven Virtures of Simple Type Theory (Farmer 2008) . I’d read it before perhaps a year ago, but decided to reread it this week. On a fundamental level, this paper is an advertisement for Higher Order Logic/Simple Type Theory as a logical framework worth using. Now, to be clear, it’s not proposing that HOL is the one true logic or anything that grandiose, but more makes a case for it being taugh as a part of standard curricula by expounding its merits.

So what are those merits? Perhaps my only complaint about the writing of this paper is that the “seven virtues” aren’t laid out clearly at the beginning but are interleaved throughout. For ease of reference then, they are

  1. simple and uniform syntax
    • propositions are just expressions of type *
    • there are very few syntactic constructs needed
      • abstraction
      • application
      • equality
      • definite choice (i.e. an operator that choose the unique element that satisfies a proposition, if it exists)
  2. it has a fairly simple semantics because the syntax is very sparse
    • the type of propositions is the two point set of true and false
    • the base types are modeled by sets
    • function types are just the total functions between sets
    • the lambda terms are interpreted the standard way
    • equality is interpreted as equality
    • definite choice is the only slightly odd one, but is interpreted as an error value if the proposition doesn’t evaluate to true for any value
  3. HOL is extremely expressive
    • quantifiers and the like can all be built up from those base elements of syntax
    • anything that can be expressed in an n-th order logic can be embedded into HOL
  4. HOL is categorical (i.e. uniquely “pins down” to a single model) for theories such as Peano Arithmetic
  5. it has a simple but very powerful proof system
    • six axioms
    • one inference rule, which is effectively simplification via equality
  6. Henkin semantics!
    • a different notion of models where the “function spaces” aren’t all the total functions
    • Henkin semantics provides many more models than the standard semantics
    • so many that we get completeness back for our proof system!
    • so many that HOL becomes fancy syntax for 1st order logic, in this perspective
  7. it has a number of neat extensions for data types, partial functions, subtypes, etc.

and that’s more or less a summary of the paper.

I really enjoyed reading this, though, as it’s very well written, easy to read, and summarizes quite a few things that I hadn’t really seen presented quite as cleanly. For example, the reduction of all the normal quantifiers and logical connectives to just the lambda calculus + equality operator and definite choice was the clearest I’d ever seen it presented. I thought the presentation in Lambek and Scott’s book (Lambek and Scott 1988) was good, but I thought this paper made it even more obvious with the simple progression at the beginning of section 4.

This paper was also the first time I’d heard of Henkin semantics, and while strictly speaking I “get it”, on a philosophic level the idea fundamentally disturbed me. I think I still have a nasty streak of platonism that I haven’t managed to expel, because the idea that there could be two very different classes of models that I’m “proving theorems about” felt very strange. It was a reminder that notions such as “completeness” are, in a sense, loosely connected to the real formal system. The logic + proof theory is capable of proving theorems. These theorems are, by our intended models, connected to “real” mathematics—whatever that’s supposed to mean. On the other hand, there are biases in our intentions, as discussed by Girard in papers such as Normativity in Logic (Girard 2012) . I suppose the more I think about this and about things such as the Lowenheim-Skolem theorem in first-order logic the more I get nervous about what the connection between our formal systems and mathematics even is.

Yes, I know, there are many practical matters where such concerns are unwarranted, but this is the part of me that I think still acts like a theologian even after all these years: constantly worried about what the ultimate truth of things is and doubting my certainty in anything.


Farmer, William M. 2008. “The Seven Virtues of Simple Type Theory.” Journal of Applied Logic 6 (3). Elsevier: 267–86.

Girard, Jean-Yves. 2012. Normativity in Logic. Springer.

Lambek, Joachim, and Philip J Scott. 1988. Introduction to Higher-Order Categorical Logic. Vol. 7. Cambridge University Press.

On Using org-ref

This is another brief post, but I wanted to talk about a tool that I’ve been appreciating a lot lately: org-ref.

The long and short of it is that this is a library that works with org-mode to help you manage citations and your bibliography. You can read the installation instructions at the org-ref github page linked above, but the basic idea is that you can insert references into your org-mode text like


and you’ll get out the actual citation properly connected to your bibliography when you export the file. You can insert citations with a key binding, mine is C-c ], and it will give you a nice little menu based on the bibtex file you have that will let you choose which reference to include. There’s also a number of helper functions that allow you to build up your bibtex file and download pdfs just from the doi or the arXiv id.

This is all cute and something I appreciate, but in some ways what I really like is that if you open the link (with C-c C-o or by clicking on it) then you also open up the associated pdf, if it exists, and open notes on that paper. Maybe it’s silly, but I was really happy about the notes because for the link above I get, in my designated notes file, something that looks like

** TODO 2009 - {Physics, Topology, Logic and Computation: A Rosetta Stone}
  :Custom_ID: 2009arXiv0903.0340B
  :AUTHOR: {Baez}, J.~C. and {Stay}, M.
  :JOURNAL: ArXiv e-prints
  :YEAR: 2009
[[cite:2009arXiv0903.0340B]] [[file:~/Dropbox/Papers//2009arXiv0903.0340B.pdf][pdf]]

which really simplifies my whole system of trying to link up papers, notes, pdfs and all of that because I used to link all of those things together manually with each paper and it was a headache. I feel like this is going to make it easier for me to write blog posts too, since I can export citations to HTML as well.

So, yeah, it’s not like you couldn’t have done all of this with elbow grease and plain bibtex, but as someone who needs a lot of organization to keep my thoughts in order this is a bit of a godsend.

The Recompiler

Today I wanted to make a brief post plugging The Recompiler, which is a new quarterly hacker magazine being launched this summer.

The way Audrey advertised the magazine to me was essentially that it was intended to be an accessible, educational, technical publication with a feminist core and I immediately asked for the opportunity to write for it.

So you might see me writing an intro to theoretical computer science piece in the near future, but regardless of that submissions are open until the end of the month, so if you think you have a topic to contribute you should absolutely submit.

Subscriptions are going to be open starting a week from today, April 21st.

Still Alive

It’s been quite awhile since I was updating regularly. A large part of that was the typical “I’ve removed the immediate emergency stressors so now my body is going to crash” thing that I think a lot of people are pretty familiar with. I was seriously ill for over a month straight starting in mid-january and since then I’ve just been chronically exhausted.

I am still alive and kicking though! This is just the massive crash that I’ve been delaying for two or three years now. I’ve started to be able to think more clearly again, the panic attacks are coming less often, and even in the middle of panic it’s getting easier to push it aside and get work done.

I’ve been doing a lot of reading, largely in trying to get caught up with the entire transcendental syntax/ludics/geometry of interaction program that I didn’t know much about until recently. They’re not the incomprehensible papers I’ve seen some (jokingly?) claim they are, but they’re dense and build on themselves. I’ve been bouncing around between Locus Solum and some of Girard’s more recent papers.

Is there some research goal that I have in mind for this reading binge of the last few weeks? Not particularly. Indeed, I’ve been trying to remind myself that I’m allowed to read things that are not within my speciality or have a clear goal to them. Sometimes it’s nice just to learn things for the sake of learning them, and the fact that it’s a topic that I find interesting and that’s making me think harder about my assumptions on logic-as-a-field is just a bonus.

Other than reading and walking so much that I’ve destroyed yet another pair of boots, I’ve still been picking away at the intro to computer science book that I’ve mentioned previously. It’s going to be in Python because that’s what my university has more-or-less standardized on, but when I asked on twitter about people’s suggestions for first programming languages I was surprised that the most common answer I got was Racket! I hadn’t really considered it as a teaching language before, despite the existence of How To Design Programs. The rest of the answers were interesting as well. More than one person suggested teaching some form of assembly language, which I’d also never considered but I can see the reasoning behind it: giving a low-level picture of how computers see computation is definitely useful. On the other hand, I seriously worry that assembly first might obscure the fundamentally algebraic character of computation. That’s my bias showing, of course, since I’m always going to lean towards understanding computation mathematically rather than as things are implemented.

So that’s basically where I am at the moment. Coming out of a long stretch of just being sick and exhausted, and getting back into the swing of things. I’m going to try and turn my beeminder goal for the blog back up again and see if we can get an honest-to-goodness posting schedule again, so we’ll see what happens!

On Scheduling or Lack Thereof

So the past couple of weeks, since my term ended, I’ve been trying to heavily schedule my days so that I don’t end up idleing or wasting my time during this leave. Yes, this was partly a medical leave which means I should be resting, but I’m not sure how easy that will ever be for me.

What I’m realizing, though, is that trying to schedule out my days in advance just really doesn’t work. I started doing it because, as I’ve written about before, I have a hard time keeping continuity in my ideas over time and making sure I don’t drop threads. I try to schedule out, a week or so in advance, all the tasks on all the various pieces of ideas that I want to keep alive. The biggest problem I’ve been having is that I can’t really predict, on any given day, what I’m going to be capable of accomplishing. This means that on most days I wake up, check my org agenda and then have to postpone most of the 12 hours of work I end up scheduling myself each day. That’s rather disheartening at first blush, but then I started thinking harder about the problem after reading Sacha Chua’s post on having a relaxed routine.

I think the real issue is not of laziness that I’ve been making a few major mistakes on trying to schedule things:

  • I’ve been pretending that there’s a way to know in advance what mental disability will allow each day
  • I’ve been overscheduling by a factor of two or three
  • I’ve had my tasks be huge things rather than small steps, e.g. “read this 120 page article on game semantics for PCF” as a single task

So I’m thinking that I need to follow something a bit more akin to the Zen To Done style of picking three important things to work on each day (or two…or one on the really bad days) and just do them. I already have all of my ideas and proposed tasks in my .org notes and a custom org-agenda view that brings up any headline starting with the keyword NEXT. That means it should be pretty easy to bring up an agenda view each morning that will let me pick a couple of things to work on each day.

When I’ve accomplished those few things, then I can take stock of how much I have left in me for the rest of the day and, if I’m all tapped out, then rest knowing that I’m still making progress. That’s one of the problems I’ve been having a lot of trouble with. At the end of the day I’m just thinking about all the things I’d hoped to do yesterday and it’s hard to just stop and take a deep breath.

Goals for the New Year

It’s probably a bit cliche to write blog posts about the new year on New Year’s Day, but it’s a ritual that I kinda like.

So I’ve already talked about the intro to programming book I want to write this year, and there’s all the drafts of papers that I was picking away at last term, so I want to get all of those things done this year but that’s not really all.

I want to do a lot more reading than I have been, both technical and non-technical. I’ve read so little fiction in the past year because I’ve barely had the energy to focus on anything when I haven’t been teaching. It’s a shame because I live in a city with one of the best library systems in the nation. I also want to read a lot more philosophy than I have. I think I’m missing a lot of the background from the more philosophic side of logic and the ways that trying to understand human reasoning inspires work in logic. I’ll be honest that I’m not entirely sure where I should begin, so if anyone has any recommendations I’ll be more than happy to take them!

I also want to sharpen my programming skills a bit since, well, I’m a good programmer and fluent in multiple languages I’m not really a master at any language in the sense of knowing the ins-and-outs of every advanced feature, trick, or technique. To that end, I really want to improve my mastery of

  • Agda
  • Idris
  • All the modern ghc-implemented Haskell extensions, since I’m mostly comfortable with Haskell 98 + multi-parameter type classes
  • C
  • Maybe OCaml and ML so I can understand the implementations of Coq and Isabelle respectively
  • Emacs lisp

Note I’m saying that I want to improve my skills in all these things, but I’m trying to be vaguely realistic about the fact that all of that plus my writing goals, a number of other research related goals, and ~1000 pages of papers to read (half of which is a couple of dissertations I want to work through) on top of this is being a medical leave means that I probably can’t accomplish everything I want in this year.

That’s a horrifying concept, really. In this time I’ve taken off to rest and heal, the idea of actually letting myself rest makes me feel sick.

So how do I figure out the real balance? I don’t know. Maybe that’s going to be a big part of what I learn this year.

Teaching Intro to Programming

So I’m on leave now, officially, but that doesn’t mean I won’t be working. I’m probably going to start teaching the intro to programming courses at my institution and, me being me, I’ve already started planning for how to do that. Why? Because even before I decided to go on leave I’d started writing my own book for the subject. I worry that seems arrogant, but I’ve looked at a number of intro to programming books and I don’t really like most of them? Basically, I want to emphasize the fundamental algebraic nature of programming and teach not just a particular language but also explain how to learn programming languages in general by way of understanding both syntax and semantics. I’m probably going to take an approach of explaining small step operational semantics without ever actually saying that’s what I’m doing. I want to emphasize that with any program you can in principle evaluate it all by hand. Now, that’s not exactly feasible for anything non-trivial but it’s a perspective that can help when learning to program. When I was first learning to code, I felt like most introductory resources made programming feel like a form of incantation. You appease the Divine Computation by using particular patterns of supplication to get the kinds of results you want and, if your prayers don’t work, you really don’t have the skills to figure out why.

I really want to try and explain, in a principled way, how every syntactic construct can be evaluated by hand and thus how to predict accurately what any piece of code is doing. I’m planning to do all of this in Python since, despite my PL-nerd ways, I want to pick a language that has a lot of local traction and, thus, community and job opportunities. Since Python isn’t referentially transparent it’s a little harder to explain how to think in terms of an operational semantics, but I have this whole approach that I used over this past summer of having the students draw out a table of values based on

  • all the variables in scope
  • the line number

and filling it out as you attempt to evaluate the program. We can introduce iterative constructs through loop unrolling forms, give functions by substitution, etc. I know that Python doesn’t have a formal semantics, but we can at least give something close enough for intuition.

Of course, that’s not all I want to try and explain in a three quarter intro sequence. I really want to explain how to read code, how to write code by figuring out the invariants that should hold and how to classify the types of variables even in an untyped language, and how to test and debug code. One of the skills that I think is important to learn is how to read a library’s, often sparse, documentation, look at the code, and thus learn how it works.

It’s going to take a couple of months to pull together a rough draft of this, but I’m planning on making it extremely example and exercise driven and I’m hoping to get a chance to refine it by having students use it once I’m back from leave.