Full Width 
Shortcuts 
Sign Up 
Log In 
Articles 
Reading List More from macwright.com
Google published Zanzibar: Google’s Consistent, Global Authorization System in 2019. It describes a system for authorization – enforcing who can do what – which maxes out both flexibility and scalability. Google has lots of different apps that rely on Zanzibar, and bigger scale than practically any other company, so it needed Zanzibar. The Zanzibar paper made quite a stir. There are at least four companies that advertise products as being inspired by or based on Zanzibar. It says a lot for everyone to loudly reference this paper on homepages and marketing materials: companies aren’t advertising their own innovation as much as simply saying they’re following the gospel. A short list of companies & OSS products I found: Companies WorkOS FGA Authzed auth0 FGA Ory Permify Open source Ory Keto (Go) Warrant (Go) probably the basis for WorkOS FGA, since WorkOS acquired Warrant. SpiceDB (Go) the basis for Authzed. Permify (Go) OpenFGA (Go) the basis of auth0 FGA. I read the paper, and have a few notes, but the Google Zanzibar Paper, annotated by AuthZed is the same thing from a real domain expert (albeit one who works for one of these companies), so read that too, or instead. Features My brief summary is that the Zanzibar paper describes the features of the system succinctly, and those features are really appealing. They’ve figured out a few primitives from which developers can build really flexible authorization rules for almost any kind of application. They avoid making assumptions about ID formats, or any particular relations, or how groups are set up. It’s abstract and beautiful. The gist of the system is: Objects: things in your data model, like documents Users: needs no explanation Namespaces: for isolating applications Usersets: groups of users Userset rewrite rules: allow usersets to inherit from each other or have other kinds of set relationships Tuples, which are like (object)#(relation)@(user), and are sort of the core ‘rule’ construct for saying who can access what There’s then a neat configuration language which looks like this in an example: name: "doc" relation { name: "owner"} relation { name: "editor" userset_rewrite { union { child { _this f } } child { computed_userset { relation: "owner" } } relation { name: "viewer" userset_rewrite { union { child {_this f} } child { computed_userset & relation: "editor" 3 } child { tuple_to_userset { tupleset { relation: "parent" } computed_userset { object: $TUPLE_USERSET_OBJECT # parent folder relation: "viewer" } } } } } } It’s pretty neat. At this point in the paper I was sold on Zanzibar: I could see this as being a much nicer way to represent authorization than burying it in a bunch of queries. Specifications & Implementation details And then the paper discusses specifications: how much scale it can handle, and how it manages consistency. This is where it becomes much more noticeably Googley. So, with Google’s scale and international footprint, all of their services need to be globally distributed. So Zanzibar is a distributed system, and it is also a system that needs good consistency guarantees so that it avoid the “new enemy” problem, nobody is able to access resources that they shouldn’t, and applications that are relying on Zanzibar can get a consistent view of its data. Pages 5-11 are about this challenge, and it is a big one with a complex, high-end solution, and a lot of details that are very specific to Google. Most noticeably, Zanzibar is built with Spanner Google’s distributed database, and Spanner has the ability to order timestamps using TrueTime, which relies on atomic clocks and GPS antennae: this is not standard equipment for a server. Even CockroachDB, which is explicitly modeled off of Spanner, can’t rely on having GPS & atomic clocks around so it has to take a very different approach. But this time accuracy idea is pretty central to Zanzibar’s idea of zookies, which are sort of like tokens that get sent around in its API and indicate what time reference the client expects so that a follow-up response doesn’t accidentally include stale data. To achieve scalability, Zanzibar is also a multi-server architecture: there are aclservers, watchservers, a Leopard indexing system that creates compressed skip list-based representations of usersets. There’s also a clever solution to the caching & hot-spot problem, in which certain objects or tuples will get lots of requests all at once so their database shard gets overwhelmed. Conclusions Zanzibar is two things: A flexible, relationship-based access control model A system to provide that model to applications at enormous scale and with consistency guarantees My impressions of these things match with AuthZed’s writeup so I’ll just quote & link them: There seems to be a lot of confusion about Zanzibar. Some people think all relationship-based access control is “Zanzibar”. This section really brings to light that the ReBAC concepts have already been explored in depth, and that Zanzibar is really the scaling achievement of bringing those concepts to Google’s scale needs. link And Zookies are very clearly important to Google. They get a significant amount of attention in the paper and are called out as a critical component in the conclusion. Why then do so many of the Zanzibar-like solutions that are cropping up give them essentially no thought? link I finished the paper having absorbed a lot of tricky ideas about how to solve the distributed-consistency problems, and if I were to describe Zanzibar, those would be a big part of the story. But maybe that’s not what people mean when they say Zanzibar, and it’s more a description of features? I did find that Permify has a zookie-like Snap Token, AuthZed/SpiceDB has ZedTokens, and Warrant has Warrant-Tokens. Whereas OpenFGA doesn’t have anything like zookies and neither does Ory Keto. So it’s kind of mixed on whether these Zanzibar-inspired products have Zanzibar-inspired implementations, or focus more on exposing the same API surface. For my own needs, zookies and distributed consistency to the degree described in the Zanzibar paper are overkill. There’s no way that we’d deploy a sharded five-server system for authorization when the main application is doing just fine with single-instance Postgres. I want the API surface that Zanzibar describes, but would trade some scalability for simplicity. Or use a third-party service for authorization. Ideally, I wish there was something like these products but smaller, or delivered as a library rather than a server.
I watched a large part of All Watched Over By Machines of Loving Grace this month. This also counts as a “listening” item, because the theme song, “Baby Love Child” by Pizzicato Five, is also spectacular. Guitar Moves is a good series of interviews by Matt Sweeney, who I mostly know via his involvement in Bonnie Prince Billy. It’s a really cool format. I like how he interviews guitarists with recognizable sounds, and you get to see how little they need to play to sound just like themselves. The episode with St. Vincent is excellent too: she’s one of my guitar heroes: check out the guitar solo in Just The Same But Brand New, or her version of Dig a Pony. I also watched No Other Land. Everyone should watch No Other Land. AI thoughts roundup I don’t have a conclusion. Really, that’s my current state: ambivalence. I acknowledge that these tools are incredibly powerful, I’ve even started incorporating them into my work in certain limited ways (low-stakes code like POCs and unit tests seem like an ideal use case), but I absolutely hate them. I hate the way they’ve taken over the software industry, I hate how they make me feel while I’m using them, and I hate the human-intelligence-insulting postulation that a glorified Excel spreadsheet can do what I can but better. Nolan Lawson: AI ambivalence As I always say, the purpose of the system is what it does. Or, in this case, how I think about AI stuff is mostly affected by how people use AI stuff, and how people use AI stuff is a real mixed bag. There’s the tidal wave of spam, the aesthetic of fascism, the low-effort marketing materials with nonsense images, the non-consensual AI porn. I see all of the bad stuff every day both online and in the odd subway ad. The good stuff seems pretty theoretical, though: the press releases about AI-driven medical advances never seem to break into the real world. The stories about engineers 10x’ing their ability seem pretty mixed: we’re already at the hangover-and-regret phase with programmers bemoaning how they’ve generated so much slop and lost so much knowledge. Anyway, I’m mildly optimistic about the potential! But it’s a lot like crypto in that you could theoretically use the technology for something good but most people loudly used it for bad stuff, and people including me judged it based on what it did. AI has to start doing some good stuff soon. Potential isn’t enough. I think one thing chatGPT’s invention has revealed is how many people - including some very important people in society - find just basic reading and writing to be laborious and cumbersome to perform, and how oddly closely that type of strained literacy correlates with having other shitty opinions. From mtsw on Bluesky, about this story about Andrew Cuomo using ChatGPT to half-assedly write a policy platform. Right off the bat I should say that judging people for their level of literacy reeks of classism and so on. My own ability to read & write has a lot to do with my place in society: I went to good schools, had a stable home life, and smart parents. However, “the way that society was set up” kind of evened this out. Extremely social people with cultural capital and chiseled jawlines and biceps would get their rewards, and people like… myself, we would get rewarded for literacy and critical thinking. When one group needed the other, it was usually some kind of payment or partnership: Cuomo pays his scriptwriter, the TV show creator pays the actors. And some people can do both sides of the equation. But LLMs definitely indicate that people do not like this deal. Whew, they don’t like writing, but they also don’t like paying the writers or reading what they write. Maybe they could rejigger the system so that they could do it all. They have ideas for music and art but no interest in learning about music, practicing instruments, going to art school, or concentrating on a task for a long time, so why not generate it all? Why not, well - there are reasons, those reasons being that the generated output usually passes their own vibe check but once someone who looks closely at things or reads all the words encounters it, everyone points at the slop and it’s embarrassing. (Cuomo will never be embarrassed) Plus, you’re always going to get average results by asking a device that is incapable of creativity or thought. Also, you’ll miss out on the human experience of creating. And you’ll be indirectly feeding output data into training data for future LLMs, consequentially making their output worse. (Cuomo does not care about consequences) Colophon update I’ve moved the images for this website to Bunny (that’s an affiliate link, here’s a non-affiliate link if that’s what you prefer). When I initially moved my photos to this website, I set them up with Amazon S3 for storage and CloudFront to serve them with a CDN. Using AWS is painful for me, so I moved them to Cloudflare R2, which is Cloudflare’s equivalent to S3, and Cloudflare as a CDN. Thanks to owning my own domains, swapping out image hosts is pretty quick: switching to Bunny took all of five minutes. So what’s the deal with Bunny? Partly I’ve become a little more negative on Cloudflare and R2: I think Cloudflare’s technology is neat, but R2 has iffy reliability and Cloudflare has iffy politics. I’m also intrigued by diversifying my dependencies geographically. Bunny is a Slovenian company, and my email is from an Australian company. This probably won’t have any practical effect, but it feels kind of good for obvious reasons to even minutely hedge my bets here. So far Bunny has been great. They don’t support the S3 protocol but they do support SFTP, which works just as well for my purposes and works great with the beautiful Transmit app. Before, with R2, I was using the significantly less beautiful Cyberduck application because Cloudflare R2 doesn’t support all of the S3 protocol. It seems to be just as fast as Cloudflare was, too. And I’m somewhat reassured by the prospect of paying Bunny. I don’t like the feeling of getting “free” services like I can from Cloudflare. I want that customer relationship. Reading Then again, pop culture is powerful, and even the dumbest marketing both affects and reflects it. Busch Light’s can holder shaped like a cup that holds beer is dumb, which is fine, because most beer promos are. But the fact that the brand frames it as a functional, masculine alternative to Stanley’s H2.0 Flowstate affirms a similarly retrograde outlook on gender roles to the one that young American men are seeking out on the political right. From my friend Dave’s article about Busch Light’s weird attempt to riff on the Stanley Tumbler trend. I was once a loyal listener of the Chapo Trap House podcast, but fell off of it in 2020 when their support of Bernie Sanders led them to be jerks about Elizabeth Warren. But reading this Vanity Fair article about the cohosts of the podcast endeared them to me a bit. “Like to thank” is linguistic phlegm. “I’d like to thank the Academy.” They’d “like to thank” me. Well I’d like to be 6’3” and drive a G Wagon, thanks. I’d like you to accept my novella. I’d like to quit paying three dollars to Submittable every time I want to send a story out. The world is full of actions I would like to do. The most direct way to say thank you is just to say it: “thank you, name, for doing X.” “I’d like to thank” is a performative thanks, a thanks with a smirk and a blink, eyeing for extra credit. Just because people say it in their award show acceptance speeches doesn’t mean you should say it, too. In fact, that’s the reason you shouldn’t say it. Loved this article “Close reading my rejections” from friend of the blog Barrett Hathcock.
Reading Whether it’s cryptocurrency scammers mining with FOSS compute resources or Google engineers too lazy to design their software properly or Silicon Valley ripping off all the data they can get their hands on at everyone else’s expense… I am sick and tired of having all of these costs externalized directly into my fucking face. Drew DeVault on the annoyance and cost of AI scrapers. I share some of that pain: Val Town is routinely hammered by some AI company’s poorly-coded scraping bot. I think it’s like this for everyone, and it’s hard to tell if AI companies even care that everyone hates them. And perhaps most recently, when a person who publishes their work under a free license discovers that work has been used by tech mega-giants to train extractive, exploitative large language models? Wait, no, not like that. Molly White wrote a more positive article about the LLM scraping problem, but I have my doubts about its positivity. For example, she suggests that Wikimedia’s approach with “Wikimedia Enterprise” gives LLM companies a way to scrape the site without creating too much cost. But that doesn’t seem like it’s working. The problem is that these companies really truly do not care. Harberger taxes represent an elegant theoretical solution that fails in practice for immobile property. Just as mobile home residents face exploitation through sudden ground rent increases, property owners under a Harberger system would face similar hold-up problems. This creates an impossible dilemma: pay increasingly burdensome taxes or surrender investments at below-market values. Progress and Poverty, a blog about Georgism, has this post about Herberger taxes, which are a super neat idea. The gist is that you would be in charge of saying how much your house is worth, but the added wrinkle is that by saying a price you are bound to be open to selling your house at that price. So if you go too low, someone will buy it, or too high, and you’re paying too much in taxes. It’s clever but doesn’t work, and the analysis points to the vital difference between housing and other goods: that buying, selling, and moving between houses is anything but simple. I’ve always been a little skeptical of the line that the AI crowd feels contempt for artists, or that such a sense is particularly widespread—because certainly they all do not!—but it’s hard to take away any other impression from a trend so widely cheered in its halls as AI Ghiblification. Brian Merchant on the OpenAI Studio Ghibli ‘trend’ is a good read. I can’t stop thinking that AI is in danger of being right-wing coded, the examples of this, like the horrifying White House tweet mentioned in that article, are multiplying. I feel bad when I recoil to innocent usage of the tool by good people who just want something cute. It is kind of fine, on the micro level. But with context, it’s so bad in so many ways. Already the joy and attachment I’ve felt to the graphic style is fading as more shitty Studio Ghibli knockoffs have been created in the last month than in all of the studio’s work. Two days later, at a state dinner in the White House, Mark gets another chance to speak with Xi. In Mandarin, he asks Xi if he’ll do him the honor of naming his unborn child. Xi refuses. Careless People was a good read. It’s devastating for Zuckerberg, Joel Kaplan, and Sheryl Sandberg, as well as a bunch of global leaders who are eager to provide tax loopholes for Facebook. Perhaps the only person who ends the book as a hero is President Obama, who sees through it all. In a March 26 Slack message, Lavingia also suggested that the agency should do away with paper forms entirely, aiming for “full digitization.” “There are over 400 vet-facing forms that the VA supports, and only about 10 percent of those are digitized,” says a VA worker, noting that digitizing forms “can take years because of the sensitivity of the data” they contain. Additionally, many veterans are elderly and prefer using paper forms because they lack the technical skills to navigate digital platforms. “Many vets don’t have computers or can’t see at all,” they say. “My skin is crawling thinking about the nonchalantness of this guy.” Perhaps because of proximity, the story that Sahil Lavingia has been working for DOGE seems important. It was a relief when a few other people noticed it and started retelling the story to the tech sphere, like Dan Brown’s “Gumroad is not open source” and Ernie Smith’s “Gunkroad”, but I have to nitpick on the structure here: using a non-compliant open source license is not the headline, collaborating with fascists and carelessly endangering disabled veterans is. Listening Septet by John Carroll Kirby I saw John Carroll Kirby play at Public Records and have been listening to them constantly ever since. The music is such a paradox: the components sound like elevator music or incredibly cheesy jazz if you listen to a few seconds, but if you keep listening it’s a unique, deep sound. Sierra Tracks by Vega Trails More new jazz! Mammoth Hands and Portico Quartet overlap with Vega Trails, which is a beautiful minimalist band. Watching This short video with John Wilson was great. He says a bit about having a real physical video camera, not just a phone, which reminded me of an old post of mine, Carrying a Camera.
I used to make little applications just for myself. Sixteen years ago (oof) I wrote a habit tracking application, and a keylogger that let me keep track of when I was using a computer, and generate some pretty charts. I’ve taken a long break from those kinds of things. I love my hobbies, but they’ve drifted toward the non-technical, and the idea of keeping a server online for a fun project is unappealing (which is something that I hope Val Town, where I work, fixes). Some folks maintain whole ‘homelab’ setups and run Kubernetes in their basement. Not me, at least for now. But I have been tiptoeing back into some little custom tools that only I use, with a focus on just my own computing experience. Here’s a quick tour. Hammerspoon Hammerspoon is an extremely powerful scripting tool for macOS that lets you write custom keyboard shortcuts, UIs, and more with the very friendly little language Lua. Right now my Hammerspoon configuration is very simple, but I think I’ll use it for a lot more as time progresses. Here it is: hs.hotkey.bind({"cmd", "shift"}, "return", function() local frontmost = hs.application.frontmostApplication() if frontmost:name() == "Ghostty" then frontmost:hide() else hs.application.launchOrFocus("Ghostty") end end) Not much! But I recently switched to Ghostty as my terminal, and I heavily relied on iTerm2’s global show/hide shortcut. Ghostty doesn’t have an equivalent, and Mikael Henriksson suggested a script like this in GitHub discussions, so I ran with it. Hammerspoon can do practically anything, so it’ll probably be useful for other stuff too. SwiftBar I review a lot of PRs these days. I wanted an easy way to see how many were in my review queue and go to them quickly. So, this script runs with SwiftBar, which is a flexible way to put any script’s output into your menu bar. It uses the GitHub CLI to list the issues, and jq to massage that output into a friendly list of issues, which I can click on to go directly to the issue on GitHub. #!/bin/bash # <xbar.title>GitHub PR Reviews</xbar.title> # <xbar.version>v0.0</xbar.version> # <xbar.author>Tom MacWright</xbar.author> # <xbar.author.github>tmcw</xbar.author.github> # <xbar.desc>Displays PRs that you need to review</xbar.desc> # <xbar.image></xbar.image> # <xbar.dependencies>Bash GNU AWK</xbar.dependencies> # <xbar.abouturl></xbar.abouturl> DATA=$(gh search prs --state=open -R val-town/val.town --review-requested=@me --json url,title,number,author) echo "$(echo "$DATA" | jq 'length') PR" echo '---' echo "$DATA" | jq -c '.[]' | while IFS= read -r pr; do TITLE=$(echo "$pr" | jq -r '.title') AUTHOR=$(echo "$pr" | jq -r '.author.login') URL=$(echo "$pr" | jq -r '.url') echo "$TITLE ($AUTHOR) | href=$URL" done Tampermonkey Tampermonkey is essentially a twist on Greasemonkey: both let you run your own JavaScript on anybody’s webpage. Sidenote: Greasemonkey was created by Aaron Boodman, who went on to write Replicache, which I used in Placemark, and is now working on Zero, the successor to Replicache. Anyway, I have a few fancy credit cards which have ‘offers’ which only work if you ‘activate’ them. This is an annoying dark pattern! And there’s a solution to it - CardPointers - but I neither spend enough nor care enough about points hacking to justify the cost. Plus, I’d like to know what code is running on my bank website. So, Tampermonkey to the rescue! I wrote userscripts for Chase, American Express, and Citi. You can check them out on this Gist but I strongly recommend to read through all the code because of the afore-mentioned risks around running untrusted code on your bank account’s website! Obsidian Freeform This is a plugin for Obsidian, the notetaking tool that I use every day. Freeform is pretty cool, if I can say so myself (I wrote it), but could be much better. The development experience is lackluster because you can’t preview output at the same time as writing code: you have to toggle between the two states. I’ll fix that eventually, or perhaps Obsidian will add new API that makes it all work. I use Freeform for a lot of private health & financial data, almost always with an Observable Plot visualization as an eventual output. For example, when I was switching banks and one of the considerations was mortgage discounts in case I ever buy a house (ha 😢), it was fun to chart out the % discounts versus the required AUM. It’s been really nice to have this kind of visualization as ‘just another document’ in my notetaking app. Doesn’t need another server, and Obsidian is pretty secure and private.
More in programming
Ten years ago, Apple’s Phil Schiller surprised Apple enthusiasts and developers by walking out on stage at John Gruber’s The Talk Show Live WWDC event and giving an open, human, honest interview to a somewhat jaded community. I wrote this in response: Both Apple and Phil Schiller himself took a huge risk in doing this. That they agreed at all is a noteworthy gift to this community of long-time enthusiasts, many of whom have felt under-appreciated as the company has grown. […] Phil’s appearance on the show was warm, genuine, informative, and entertaining. It was human. And humanizing the company and its decisions, especially to developers — remember, developer relations is all under Phil — might be worth the PR risk. This started a ten-year run of interviews by Apple executives on The Talk Show every year at WWDC that proved to be great, surprisingly safe PR for Apple. No executive ever said something they shouldn’t have (they’re pros), no sensational or negative news stories ever resulted from them, and Apple’s enthusiastic fans and developers felt seen, heard, and appreciated. * * * For unspecified reasons, Apple has declined to participate this year, ending what had become a beloved tradition in our community — and I can’t help but suspect that it won’t come back. (A lot has changed in the meantime.) Maybe Apple has good reasons. Maybe not. We’ll see what their WWDC PR strategy looks like in a couple of weeks. In the absence of any other information, it’s easy to assume that Apple no longer wants its executives to be interviewed in a human, unscripted, unedited context that may contain hard questions, and that Apple no longer feels it necessary to show their appreciation to our community and developers in this way. I hope that’s either not the case, or it doesn’t stay the case for long. This will be the first WWDC I’m not attending since 2009 (excluding the remote 2020 one, of course). Given my realizations about my relationship with Apple and how they view developers, I’ve decided that it’s best for me to take a break this year, gain some perspective, and decide what my future relationship should look like. Maybe Apple’s leaders are doing that, too.
Thinking about moving to Japan? You’re not alone—Japan is a popular destination for those hoping to move abroad. What’s more, Japan actually needs more international developers. But how easy is it to immigrate to and work in Japan? Scores of videos on social media warn that living in Japan is quite different from holidaying here, and graphic descriptions of exploitative companies also create doubt. The truth is that Japan is not the easiest country to immigrate to, nor is it the hardest. Some Japanese tech companies and developer roles offer great work-life balance and good compensation; others do not. Based on other developers’ experiences, you’ll thrive here if you: Are an experienced developer Value safety, good food, and convenience over a high salary Are willing to invest time and effort into learning Japanese over the long term Read on to discover if Japan is a good fit for you, and the best ways to get a visa and begin your life here. What is it like working as a developer in Japan? TokyoDev conducts an annual survey of international developers living in Japan. Many of the questions in TokyoDev’s 2024 survey specifically addressed respondents’ work environments. Compensation When TokyoDev asked about “workplace difficulties” in the 2024 survey, 45% of respondents said that “compensation” was their number one problem at work. Overall, compensation for developers in Japan is far lower than the US developer median salary of 120,000 USD (currently 17.5 million yen), but higher than the Indian developer median salary of 640,000 rupees (currently around 1.1 million yen). Yet evaluating compensation for international developers in Japan, specifically, is trickier than you might expect. It’s hard to define an expected salary range because international developers tend to work in different companies and roles than the average Japanese developer. According to a 2024 survey conducted by the Japanese Ministry of Health, Labor and Welfare, the average annual salary of software engineers in Japan was 5.69 million yen. In a survey conducted that same year by TokyoDev, though, English-speaking international software developers in Japan enjoyed a median salary of 8.5 million yen. Of those international developers who responded, only 71% of them worked at a company headquartered in Japan, and almost 80% of them used English always or frequently, with 79% belonging to an engineering team with many other non-Japanese members. Wages, then, are heavily influenced by a range of factors, but particularly by whether you’re working for a Japanese or international company. In general, 75% of the international developers surveyed made 6 million yen or more. The real question is, is that enough for you to be comfortable in Japan? The answer is likely to be yes, if you don’t have overseas financial obligations or dependents. If you do, you’ll want to look carefully at rent, grocery, and education prices in your area of choice to guesstimate the expense of your Japanese lifestyle. Work-life balance Japan has a tradition of long hours and overtime. The Financial Times reports that the Japanese government has taken many measures to reduce the phenomenon of death from overwork (過労死, karoushi), from capping overtime to 100 hours a month, to setting up a national hotline for employees to report abusive companies. The results seem mixed. The Financial Times article adds that in 2024, employees at 26,000 organizations reported working illegal overtime at 44.5% of those businesses. On the other hand, average working hours for men fell to below 45 hours per week, and for women to below 35, which is similar to average working hours in the US. Still, 72% of the developers surveyed by TokyoDev worked for less than 40 hours a week. In addition, 70% of TokyoDev respondents cited work-life balance as their top workplace perk. The number of respondents happy with their working conditions came in just below that, at 69%. There was some correlation between hours worked and the type of employer, though. Employees at international subsidiaries were slightly more likely to enjoy shorter work weeks than those at Japanese companies. Remote work Remote work is still relatively new in Japan. Although more offices adopted the practice during Covid, many of them are now backtracking and requiring employees to return to the office, often with a hybrid schedule. While only 9% of TokyoDev respondents weren’t allowed any remote work, 76% of those required to work in-office were employed by Japan-headquartered companies. By contrast, of the 16% who worked fully remotely, only 57% worked for a Japanese company. Those with the option to work remotely really enjoy it. When asked what their most important workplace benefit was, 49% of respondents answered “remote work,” outstripping every other answer by far. Job security A major plus of working in Japan is job security—which, given the waves of layoffs at American tech companies, may now seem extra appealing. It’s overwhelmingly difficult to fire or lay off an employee with a permanent contract (正社員, seishain) in Japan, due to labor laws designed to protect the individual. This may be why 54% of TokyoDev survey respondents named “job security” as their most important workplace perk. Not every company will adhere to labor protection laws, and sometimes businesses pressure employees to “voluntarily” resign. Nonetheless, employees have significant legal recourse when companies attempt to fire them, change their contracts, or alter the current workplace conditions (sometimes, even if those conditions were never stated in writing). Developer stories TokyoDev regularly interviews developers working at our client companies, for information on both their specific positions and their general work environment. Our interviewees work with a variety of technology in many different roles, and at companies ranging from fintech enterprises like PayPay to game companies like Wizcorp. Why do developers choose Japan? In 2024 TokyoDev also asked developers, “What’s your favorite thing about Japan?” The results were: Safety: 21% Food: 13% Convenience: 11% Culture: 8% Peacefulness: 7% Nature: 5% Interestingly, there was a strong correlation between the amount of time someone had lived in Japan and their answer. Those who had been in Japan three years or less more frequently chose “food” or “culture.” Those who’d lived in Japan for four or more years were significantly more likely to answer “safety” or “peacefulness.” Safety It’s true that Japan enjoys a lower crime rate than many developed nations. The Security Journal UK ranked it ninth in a list of the world’s twenty safest countries. In 2024, World Population Review selected Tokyo as the safest city in the world. The homicide rate in 2023 was only 0.23 per 100,000 people, and has been steadily declining since the nineties. There are a few women-specific concerns, such as sexual violence. Nonetheless, the subjective experience of many women in the TokyoDev audience is that Japan feels safe; for example, they experience no trepidation walking around late at night. Of course, crime statistics don’t take into account natural disasters, of which Japan has more than its fair share. Thanks to being located on the Ring of Fire, Japan regularly copes with earthquakes and volcanic activity, and its location in the Pacific means that it is also affected by typhoons and tsunamis. To compensate, Japan also takes natural disaster countermeasures extremely seriously. It’s certainly the only country I’ve been to that posts large-scale evacuation maps on the side of the street, stores emergency supply stockpiles in public parks, and often requires schoolchildren to keep earthquake safety headgear at their desks. Food Food is another major draw. Many respondents simply wrote that “food” or “fresh, affordable food” was their favorite thing about Japan, but a few listed specific dishes. Favorite Japanese foods of the TokyoDev audience include: Yakiniku (self-grilled meat) Ramen Peaches Sushi Hiroshima-style okonomiyaki (savory pancake) Curry rice Onigiri (rice balls) Of those, sushi was mentioned most often. One respondent also answered the question with “drinking,” if you think that should count! Personal experiences Our contributors have also shared their personal experiences of moving to and working in Japan. We’ve got articles from Filipino, Indonesian, Australian, Vietnamese, and Mongolian developers, as well as others sharing what it’s like to work as a female software developer in Japan, or to live in Japan with a disability. Why shouldn’t you live in Japan? Safety, food, convenience, and culture are the most commonly-cited upsides of living in Japan. The downsides are the necessity of learning the language and some strict, yet often-unspoken, cultural expectations. Language Fluency in Japanese is not strictly necessary to live or work in Japan. Access to government services for you and your family, such as Japanese public school, is possible even if you speak little Japanese. (That doesn’t mean that most city hall clerks speak English; usually they’ll either locate a translator, or work with you via a translation app.) Nonetheless, TokyoDev’s 2024 survey showed that language ability was highly correlated to social success in Japan. In particular, 56% of all respondents were happy or very happy with their adjustment to Japanese culture. Breaking down that number, though, 76% of those with fluent or native Japanese ability reported being happy with their cultural adjustment, while only 34% of those with little or no Japanese ability were similarly happy. The same held true for social life satisfaction: 59% of those with fluent or native Japanese ability were happy or very happy with their social life, compared to 42% of those who don’t speak much Japanese. While English study is compulsory in Japan and starts in elementary school, as of 2025, only 28% of Japanese people speak English, and most of them can’t converse with high fluency. Living and working in Japan is possible without Japanese, but it’s hard to integrate, make friends, and participate in cultural activities if you can’t communicate with the locals. Cultural expectations As mentioned above, fluency in Japanese is closely allied to fluency in Japanese culture. At the same time, one does not necessarily imply the other. It’s possible to be fluent in Japanese, but still not grasp many of the unspoken rules your Japanese friends, neighbors, and coworkers operate by. Japan’s culture is both high-context and specifically averse to confrontation and outspokenness; if you get it “wrong,” people aren’t likely to tell you so. Japanese culture also values conformity: as the saying goes, “the nail that sticks up, gets hammered down.” While there are hints of things changing, with many Japanese companies saying support for greater diversity is necessary, minorities or those who are different may experience pressure to fit in. Introspection is required: are you the kind of person who’s adept at “reading the room,” a highly-valued quality in Japan? Conversely, are you self-confident enough to not sweat the small stuff? Either of these personality types may do well in Japan, but if social acceptance is very important to you, and you’re also uncomfortable with feeling occasionally awkward or uncertain, then you may struggle more to adjust. I want to go! How can I get there? If you’ve decided to immigrate to Japan, there are a number of ways to acquire a work visa. The simplest way is to get hired by a company operating in Japan. Alternatively, you can start your own business in Japan, come over on a Working Holiday, or even—if you’re very determined—arrive first as an English teacher. Let’s begin with the most straightforward route: getting hired as a developer. Getting a developer job in Japan As mentioned before, Japan needs more international developers. Some types of developers, though, will find it easier to get a job in Japan. In particular, companies in Japan are looking for the following: Senior developers. Companies are particularly interested in those with management experience and soft skills such as communication and leadership. Backend developers. This is one of the most widely-available roles for those who don’t speak Japanese. Developers who know Python. Python is one of Japan’s top in-demand languages. AI and Machine Learning Specialists. Japan is leaning hard on AI to help cope with demographic changes. Those who already know, or are willing to learn, Japanese. Combining those criteria, an experienced developer who speaks Japanese should have little difficulty finding a job! If you’re none of these things, you don’t need to give up—you just need to be patient, flexible, and willing to think outside the box. As Mercari Senior Technical Recruiter Clement Chidiac told me, “I know a bunch of people that managed to land a job because they’ve tried harder, going to meetups, reaching out to people, networking, that kind of thing.” Edmund Ho, Principal Consultant at Talisman Corporation, agreed that overseas candidates hoping to work in Japan for the first time face a tough road. He believes candidates should maintain a realistic, but optimistic, view of the process. “Keep a longer mindset,” he suggested. “Maybe you don’t get an offer the first year, but you do the second year.” “Stepping-stone” jobs Candidates from overseas do face a severe disadvantage: many companies, even those founded by non-Japanese people, are only open to developers who already live in Japan. Although getting a work visa for an overseas employee is cheaper and easier in Japan than in many countries, it still presents a barrier some organizations are reluctant to overcome. By contrast, once you’re already on the ground, more companies will be interested in your skills. This is why some developers settle on a “stepping-stone” position—in other words, a job that may not be all you hoped for, but that is willing to sponsor your visa and bring you into the country. Here’s where some important clarification on Japanese work visas is required. Work visas The most common visa for developers is the Engineer/Specialist in Humanities/International Services visa, a broad-category visa for foreign workers in those fields. To qualify, a developer must have a college degree, or have ten years of work experience, or have passed an approved IT exam. Another relatively common visa for high-level developers is the Highly-Skilled Professional (HSP) visa. To acquire it, applicants must score at least 70 points on an assessment scale that addresses age, education level, Japanese level, income, and more. The HSP visa has many advantages, but there is one important difference between it, and the more standard Engineer visa. The Engineer/Specialist in Humanities/International Services visa is not tied to a specific company. It grants you the legal right to work within those fields for a specific period of time in Japan. The Highly-Skilled Foreign Professional visa, on the other hand, is tied to a specific employer. If you want to change jobs, you’ll need to update your residency status with immigration. Some unscrupulous companies will try to claim that because they sponsored your Engineer/Specialist in Humanities/International Servicesvisa, you are obligated to remain with their company or risk being deported. This is not the case. If you do leave your job without another one lined up, you have three months to find another before you may be at risk for deportation. In addition, the fields of work covered by the Engineer/Specialist in Humanities/International Services visa are incredibly broad, and include everything from sales to product development to language instruction. As TokyoDev specifically confirmed with immigration, you can even come to Japan as an English instructor, then later work as a developer, without needing to alter your visa. Those with the HSP visa will need to go to immigration and alter their residency status each time they change roles. However, if you have the points and qualifications for an HSP visa, that means you’re also eligible for Permanent Residency within one to three years. Once you’ve obtained Permanent Residency, you’re free to pursue whatever sort of employment you like. International or Japanese company? As you begin your job hunt, you’ll hopefully receive responses from several sorts of companies: Japanese companies that also primarily hire Japanese people, Japanese companies with designated multinational developer teams, companies that were founded in Japan but nonetheless hire international developers for a variety of positions, and international subsidiaries. There are advantages and disadvantages to working with mostly-Japanese or mostly-international companies. Japanese companies The more Japanese a company is—both in philosophy and personnel—the more you’ll need Japanese language skills to thrive there. It’s true that a number of well-established Japanese tech companies are now creating developer teams designed to be multinational from the outset: typically, these are very English-language friendly. Some organizations, such as Money Forward, have even adopted English as the official company language. However, this often results in an institutional language barrier between development teams and the rest of the company, which is usually staffed by Japanese speakers. Developers are still encouraged to learn Japanese, particularly as they climb the promotional ladder, to help facilitate interdepartmental communication. Some companies, such as DeepX and Beatrust, either offer language classes themselves or provide a stipend for language learning. In addition to the language, you’ll also need to become “fluent” in Japanese business norms, which can be much more rigid and hierarchical than American or European company cultures. For example, at introductory drinking parties (themselves a potential surprise for many!), it is customary for new employees or women employees to go around with a bottle of beer and pour glasses for their managers and the company’s senior management. As mentioned in the cultural expectations section, most Japanese people won’t correct you even if you’re doing it all wrong, which leaves foreigners to discover their gaffes via trial-and-error. The advantage here is that you’ll be pressured, hopefully in a good way, to adapt swiftly to the Japanese language and business culture. There’s a sink-or-swim element to this approach, but if you’re serious about settling in Japan, then this “downside” could benefit you in the long run. Finally, there is the above-mentioned issue of compensation. On average, international companies pay more than Japanese ones; the median salary difference is around three million yen per year. Specific roles may be paid at higher rates, though, and most Japanese companies do offer bonuses. Many Japanese companies also offer other perks, such as housing stipends, spouse and child allowances, etc. If you receive an offer, it’s worth examining the whole compensation package before you make a decision. International companies The advantages of working either for an international company, or for a Japanese company that already employs many non-Japanese people, are straightforward: you can usually communicate in English, you already understand most of the business norms, and such companies typically pay developers more. You do run the risk of getting stuck in a rut, though. As mentioned earlier, TokyoDev found in its own survey that the correlation between Japanese language skills and social life satisfaction is high. You can of course study Japanese in your free time—and many do—but the more your work environment and social life revolve around English, the more difficult acquiring Japanese becomes. Want a job? Start here! If you’re ready to begin your job hunt, you can start with the TokyoDev job board. TokyoDev only works with companies we feel good about sending applicants to, and the job board includes positions that don’t require Japanese and that accept candidates from abroad. Other alternatives These visas don’t lead directly to working as a software developer in Japan, but can still help you get your foot in the door. DIY options If you prefer to be your own boss, there are several visas that allow you to set up a business in Japan. The Business Manager visa is typically good for one year, although repeated applicants may get longer terms. Applicants should have five million yen in a bank account when they apply, and there are some complicated requirements for getting and keeping the visa, such as maintaining an office, paying yourself a minimum salary, following proper accounting procedures, etc. The Startup visa is another option if the Business Manager visa appeals to you, but you don’t yet have the funds or connections to make it happen. You’ll be granted the equivalent of a Business Manager visa for up to one year so that you can launch your business in Japan. Working Holiday visa This is the path our own founder Paul McMahon took to get his first developer job in Japan. If you meet various qualifications, and you belong to a country that has a Working Holiday visa agreement with Japan, you can come to Japan for a period of one year and do work that is “incidental” to your holiday. In practice, this means you can work almost any job except for those that are considered “immoral” (bars, clubs, gambling, etc.). The Working Holiday visa is a great opportunity for those who have the option. It allows you to experience living and working in Japan without any long-term commitments, and also permits you to job-hunt freely without time or other visa constraints. J-Find visa The J-Find visa is a one-year visa, intended to let graduates of top universities job-hunt or prepare to found a start-up in Japan. To qualify, applicants should have: A degree from a university ranked in the top 100 by at least two world university rankings, or completed a graduate course there Graduated within five years of the application date At least 200,000 yen for initial living expenses TokyoDev contributor Oguzhan Karagözoglu received a J-Find visa, though he did run into some difficulties, particularly given immigration’s unfamiliarity with this relatively new type of visa. Digital Nomad visa This is another new visa category that allows foreigners from specific countries, who must make over 10 million yen or more a year, to work remotely from Japan for six months. Given that the application process alone can take months, the visa isn’t extendable or renewable, and you’re not granted residency, it’s questionable whether the pay-off is worth the effort. Still, if you have the option to work remotely and want to test out living in Japan before committing long-term, this is one way to do that. TokyoDev contributor Christian Mack was not only one of the first to acquire the Digital Nomad visa, but has since opened a consultancy to help others through the process. Conclusion If your takeaway from this article is, “Japan, here I come!” then there are more TokyoDev articles that can help you on your way. For example, if you want to bring your pets with you, you should know that you need to start preparing the import paperwork up to seven months in advance. If you’re ready now to start applying for jobs, check out the TokyoDev job board. You’ll also want to look at how to write a resume for a job in Japan, and our industry insider advice on passing the resume screening process. These tips for interviewing at Japanese tech companies would be useful, and when you’re ready for it, see this guide to salary negotiations. Once you’ve landed that job, we’ve got articles on everything from bringing your family with you, to getting your first bank account and apartment. In addition, the TokyoDev Discord hosts regular discussions on all these topics and more. It’s a great chance to make developer friends in Japan before you ever set foot in the country. Once you are here, you can join some of Japan’s top tech meetups, including many organized by TokyoDev itself. We look forward to seeing you soon!
We go over the "Wake up, Remix!" article by the remix team and talk about their decisions moving forward and also speculate on what is coming next.
TIL (or this week-ish I learned) why big-sigma and big-pi turn up in the notation of dependent type theory. I’ve long been aware of the zoo of more obscure Greek letters that turn up in papers about type system features of functional programming languages, μ, Λ, Π, Σ. Their meaning is usually clear from context but the reason for the choice of notation is usually not explained. I recently stumbled on an explanation for Π (dependent functions) and Σ (dependent pairs) which turn out to be nicer than I expected, and closely related to every-day algebraic data types. sizes of types The easiest way to understand algebraic data types is by counting the inhabitants of a type. For example: the unit type () has one inhabitant, (), and the number 1 is why it’s called the unit type; the bool type hass two inhabitants, false and true. I have even seen these types called 1 and 2 (cruelly, without explanation) in occasional papers. product types Or pairs or (more generally) tuples or records. Usually written, (A, B) The pair contains an A and a B, so the number of possible values is the number of possible A values multiplied by the number of possible B values. So it is spelled in type theory (and in Standard ML) like, A * B sum types Or disjoint union, or variant record. Declared in Haskell like, data Either a b = Left a | Right b Or in Rust like, enum Either<A, B> { Left(A), Right(B), } A value of the type is either an A or a B, so the number of possible values is the number of A values plus the number of B values. So it is spelled in type theory like, A + B dependent pairs In a dependent pair, the type of the second element depends on the value of the first. The classic example is a slice, roughly, struct IntSlice { len: usize, elem: &[i64; len], } (This might look a bit circular, but the idea is that an array [i64; N] must be told how big it is – its size is an explicit part of its type – but an IntSlice knows its own size. The traditional dependent “vector” type is a sized linked list, more like my array type than my slice type.) The classic way to write a dependent pair in type theory is like, Σ len: usize . Array(Int, len) The big sigma binds a variable that has a type annotation, with a scope covering the expression after the dot – similar syntax to a typed lambda expression. We can expand a simple example like this into a many-armed sum type: either an array of length zero, or an array of length 1, or an array of length 2, … but in a sigma type the discriminant is user-defined instead of hidden. The number of possible values of the type comes from adding up all the alternatives, a summation just like the big sigma summation we were taught in school. ∑ a ∈ A B a When the second element doesn’t depend on the first element, we can count the inhabitants like, ∑ A B = A*B And the sigma type simplifies to a product type. telescopes An aside from the main topic of these notes, I also recently encountered the name “telescope” for a multi-part dependent tuple or record. The name “telescope” comes from de Bruijn’s AUTOMATH, one of the first computerized proof assistants. (I first encountered de Bruijn as the inventor of numbered lambda bindings.) dependent functions The return type of a dependent function can vary according to the argument it is passed. For example, to construct an array we might write something like, fn repeat_zero(len: usize) -> [i64; len] { [0; len] } The classic way to write the type of repeat_zero() is very similar to the IntSlice dependent pair, but with a big pi instead of a big sigma: Π len: usize . Array(Int, len) Mmm, pie. To count the number of possible (pure, total) functions A ➞ B, we can think of each function as a big lookup table with A entries each containing a B. That is, a big tuple (B, B, … B), that is, B * B * … * B, that is, BA. Functions are exponential types. We can count a dependent function, where the number of possible Bs depends on which A we are passed, ∏ a ∈ A B a danger I have avoided the terms “dependent sum” and “dependent product”, because they seem perfectly designed to cause confusion over whether I am talking about variants, records, or functions. It kind of makes me want to avoid algebraic data type jargon, except that there isn’t a good alternative for “sum type”. Hmf.
Systems Distributed I'll be speaking at Systems Distributed next month! The talk is brand new and will aim to showcase some of the formal methods mental models that would be useful in mainstream software development. It has added some extra stress on my schedule, though, so expect the next two monthly releases of Logic for Programmers to be mostly minor changes. What does "Undecidable" mean, anyway Last week I read Against Curry-Howard Mysticism, which is a solid article I recommend reading. But this newsletter is actually about one comment: I like to see posts like this because I often feel like I can’t tell the difference between BS and a point I’m missing. Can we get one for questions like “Isn’t XYZ (Undecidable|NP-Complete|PSPACE-Complete)?” I've already written one of these for NP-complete, so let's do one for "undecidable". Step one is to pull a technical definition from the book Automata and Computability: A property P of strings is said to be decidable if ... there is a total Turing machine that accepts input strings that have property P and rejects those that do not. (pg 220) Step two is to translate the technical computer science definition into more conventional programmer terms. Warning, because this is a newsletter and not a blog post, I might be a little sloppy with terms. Machines and Decision Problems In automata theory, all inputs to a "program" are strings of characters, and all outputs are "true" or "false". A program "accepts" a string if it outputs "true", and "rejects" if it outputs "false". You can think of this as automata studying all pure functions of type f :: string -> boolean. Problems solvable by finding such an f are called "decision problems". This covers more than you'd think, because we can bootstrap more powerful functions from these. First, as anyone who's programmed in bash knows, strings can represent any other data. Second, we can fake non-boolean outputs by instead checking if a certain computation gives a certain result. For example, I can reframe the function add(x, y) = x + y as a decision problem like this: IS_SUM(str) { x, y, z = split(str, "#") return x + y == z } Then because IS_SUM("2#3#5") returns true, we know 2 + 3 == 5, while IS_SUM("2#3#6") is false. Since we can bootstrap parameters out of strings, I'll just say it's IS_SUM(x, y, z) going forward. A big part of automata theory is studying different models of computation with different strengths. One of the weakest is called "DFA". I won't go into any details about what DFA actually can do, but the important thing is that it can't solve IS_SUM. That is, if you give me a DFA that takes inputs of form x#y#z, I can always find an input where the DFA returns true when x + y != z, or an input which returns false when x + y == z. It's really important to keep this model of "solve" in mind: a program solves a problem if it correctly returns true on all true inputs and correctly returns false on all false inputs. (total) Turing Machines A Turing Machine (TM) is a particular type of computation model. It's important for two reasons: By the Church-Turing thesis, a Turing Machine is the "upper bound" of how powerful (physically realizable) computational models can get. This means that if an actual real-world programming language can solve a particular decision problem, so can a TM. Conversely, if the TM can't solve it, neither can the programming language.1 It's possible to write a Turing machine that takes a textual representation of another Turing machine as input, and then simulates that Turing machine as part of its computations. Property (1) means that we can move between different computational models of equal strength, proving things about one to learn things about another. That's why I'm able to write IS_SUM in a pseudocode instead of writing it in terms of the TM computational model (and why I was able to use split for convenience). Property (2) does several interesting things. First of all, it makes it possible to compose Turing machines. Here's how I can roughly ask if a given number is the sum of two primes, with "just" addition and boolean functions: IS_SUM_TWO_PRIMES(z): x := 1 y := 1 loop { if x > z {return false} if IS_PRIME(x) { if IS_PRIME(y) { if IS_SUM(x, y, z) { return true; } } } y := y + 1 if y > x { x := x + 1 y := 0 } } Notice that without the if x > z {return false}, the program would loop forever on z=2. A TM that always halts for all inputs is called total. Property (2) also makes "Turing machines" a possible input to functions, meaning that we can now make decision problems about the behavior of Turing machines. For example, "does the TM M either accept or reject x within ten steps?"2 IS_DONE_IN_TEN_STEPS(M, x) { for (i = 0; i < 10; i++) { `simulate M(x) for one step` if(`M accepted or rejected`) { return true } } return false } Decidability and Undecidability Now we have all of the pieces to understand our original definition: A property P of strings is said to be decidable if ... there is a total Turing machine that accepts input strings that have property P and rejects those that do not. (220) Let IS_P be the decision problem "Does the input satisfy P"? Then IS_P is decidable if it can be solved by a Turing machine, ie, I can provide some IS_P(x) machine that always accepts if x has property P, and always rejects if x doesn't have property P. If I can't do that, then IS_P is undecidable. IS_SUM(x, y, z) and IS_DONE_IN_TEN_STEPS(M, x) are decidable properties. Is IS_SUM_TWO_PRIMES(z) decidable? Some analysis shows that our corresponding program will either find a solution, or have x>z and return false. So yes, it is decidable. Notice there's an asymmetry here. To prove some property is decidable, I need just to need to find one program that correctly solves it. To prove some property is undecidable, I need to show that any possible program, no matter what it is, doesn't solve it. So with that asymmetry in mind, do are there any undecidable problems? Yes, quite a lot. Recall that Turing machines can accept encodings of other TMs as input, meaning we can write a TM that checks properties of Turing machines. And, by Rice's Theorem, almost every nontrivial semantic3 property of Turing machines is undecidable. The conventional way to prove this is to first find a single undecidable property H, and then use that to bootstrap undecidability of other properties. The canonical and most famous example of an undecidable problem is the Halting problem: "does machine M halt on input i?" It's pretty easy to prove undecidable, and easy to use it to bootstrap other undecidability properties. But again, any nontrivial property is undecidable. Checking a TM is total is undecidable. Checking a TM accepts any inputs is undecidable. Checking a TM solves IS_SUM is undecidable. Etc etc etc. What this doesn't mean in practice I often see the halting problem misconstrued as "it's impossible to tell if a program will halt before running it." This is wrong. The halting problem says that we cannot create an algorithm that, when applied to an arbitrary program, tells us whether the program will halt or not. It is absolutely possible to tell if many programs will halt or not. It's possible to find entire subcategories of programs that are guaranteed to halt. It's possible to say "a program constructed following constraints XYZ is guaranteed to halt." The actual consequence of undecidability is more subtle. If we want to know if a program has property P, undecidability tells us We will have to spend time and mental effort to determine if it has P We may not be successful. This is subtle because we're so used to living in a world where everything's undecidable that we don't really consider what the counterfactual would be like. In such a world there might be no need for Rust, because "does this C program guarantee memory-safety" is a decidable property. The entire field of formal verification could be unnecessary, as we could just check properties of arbitrary programs directly. We could automatically check if a change in a program preserves all existing behavior. Lots of famous math problems could be solved overnight. (This to me is a strong "intuitive" argument for why the halting problem is undecidable: a halt detector can be trivially repurposed as a program optimizer / theorem-prover / bcrypt cracker / chess engine. It's too powerful, so we should expect it to be impossible.) But because we don't live in that world, all of those things are hard problems that take effort and ingenuity to solve, and even then we often fail. To be pendantic, a TM can't do things like "scrape a webpage" or "render a bitmap", but we're only talking about computational decision problems here. ↩ One notation I've adopted in Logic for Programmers is marking abstract sections of pseudocode with backticks. It's really handy! ↩ Nontrivial meaning "at least one TM has this property and at least one TM doesn't have this property". Semantic meaning "related to whether the TM accepts, rejects, or runs forever on a class of inputs". IS_DONE_IN_TEN_STEPS is not a semantic property, as it doesn't tell us anything about inputs that take longer than ten steps. ↩
