So it’s been a pretty good year over here. After four years in California I finally feel like I live here and I get to have my own life now, instead of performing some version of the life that I thought I wanted when I moved out here. My stress levels have been a lot lower and I’ve had time and energy after work to really develop my own interests.

I got a new job this year (Software Engineer at Chartio) and it’s helped clarify what I really enjoy out of work. I’ve worked enough different places now to get a feel for the types of projects I enjoy the most. These projects tend to be situations where I have a lot of autonomy while I get to learn a lot at the same time, and the new job lets me have that more often than not, fulltime. Pretty nice.

Another thing that’s quite nice is the company size - I really like a smaller team size. Tilt and Lyft oriented their teams around product verticals which may be the way you need to organize once you get to a certain size, but it’s not enjoyable to have any of the “my team” vs “your team” that comes out of a structure like that (works great if you’re on “my team” and never have to deal with “your team” I guess). It’s also really nice to have the more direct line to the customers that comes in a smaller environment.

I ended up doing some recreational coding. I did the first few Cryptopals problem sets in April using OCaml, implemented Berklekamp and Cantor-Zassanhaus Factorization for polynomials over finite fields in Golang for reasons I still can’t identify, and returned to my new Golang chess engine that I started last year. Ra (new engine) still consistently loses to Apep (my old C++ chess engine) but I’m pretty sure I can change that with a bit more work. Chess engines are super fun and they make me want to develop my chess skills so I can handle myself a little better over the board. Maybe one day I’ll get to writing some articles on chess programming up.

I also dedicated a bunch of time to improving my abilities with Coq. I read through Interactive Theorem Proving and Program Development and more or less grok everything in it. I completed my proof of grade-school arithmetic (started last year). After going through all the teeth-pulling that it takes to formalize proving base 10 addition with carry-over is the same as the built-in addition operator, I’m not sure how mainstream theorem proving will ever be. Obviously the startup world where I work has major issues to solve before it gets to certifying the correctness of our programs, but it feels impractical even in fields where it might ostensibly make sense, such as professional mathematics. The idea that modern math papers could come with a program proving it correct is extremely far out of reach, or at least that dependent typing isn’t the right tool for the job. It would take a herculean effort to certify the first 30 pages of one of the number theory textbooks that I read.

I did some reading. I finally read Ursula Le Guin, though unfortunately she had to die to get herself high enough on my radar. The Left Hand of Darkness was a wonderful book and I find myself wanting to return to its world (maybe in the new year). One of my goals for the Christmas break is to read through a few of her Earthsea books. I really liked The Dispossessed, which I interpreted as her take on The Fountainhead. I think it’s important for us whose politics are on the left to understand how the themes in The Fountainhead resonate with people, even if we disagree with the ends that its author turns them towards. Shevek is a brilliant scientist who is stranded in a backwater where he can’t work except as servant to a university elder. He rejects his homeland to join the place where “real science” is done, but then discovers he is nothing but a pawn of those in power, and must rebel again. Great stuff.

I also read the first four Dune novels. I’m not sure why it took me this long to get around to it - it was sort of intimidating, I guess. Afterwards, it’s easy to see its fingerprints over many of my favorite sci-fi/fantasy worlds. The one I spent the most time thinking about was Miyazaki’s Nausicaa of the Valley of the Wind (there’s a movie, but like any true nerd I’ll tell you the manga is way better). Nausicaa is a very similar protagonist in some ways but makes very different choices from the Atreides madmen. After the first Dune book, the Atreides consistently embrace autocracy over allowing the common people a voice, usually justifying it by some imagined horrific future that never seems to manifest. Nausicaa chooses differently - she rejects the mantle of rulership, and given the opportunity to remake her world into a paradise (like the Atreides eventually do for Arrakis), she destroys the tools of the past that the ruling class uses to dominate the world (while the Atreides horde the spice to cement their rule). Our world could use a lot more of Nausicaa and a lot less of the Atreides.

And of course, I did some surgery on this blog. I de-listed a bunch of older articles that didn’t age well for one reason or another. Either I now disagreed with them, didn’t think they made their points very well, or they just weren’t unique enough. One of my favorite internet jokes is Clickhole’s “The Time I Spent On A Commercial Whaling Ship Totally Changed My Perspective On The World”, where all of Melville’s beautiful prose in Moby Dick gets turned into the doggerel of the internet just by being presented on a webpage. There are enough programming blogs out there that talk about stuff you did in the context of work and isn’t work/my company/my team just the greatest. I feel a little embarrassed by my past contribution to the genre but I’m doing my best to turn this little corner of the internet into as weird and unique a place as I can possibly make it. Not sure where that will go but I guess that’s the point. Best wishes for a great 2019, all.