Remote

Colin Gordon

@csgordon@discuss.systems

mastodon 4.7.3

Programming languages professor, kernel hacker, aspiring linguist (syntax & compositional semantics).

Currently figuring out how to combine all of my interests by mechanically translating English into formal specifications of a formally verified OS kernel for RISC-V.

503 Followers

1504 Following

35 Posts

Joined August 08, 2023

pronouns:

he/him, er/ihn

languages:

english (native), deutsch (~B2, Ich spreche ein bisschen Deutsch, aber nicht genug für alles zu benutzen), français (<A1, je parle seulement un peut le français), linguae latinae (relearning bit-rotted ~B1)

alts:

@csgordon@mathstodon.xyz and @csgordon@lingo.lol

homepage:

https://csgordon.github.io/

Colin Gordon @csgordon@discuss.systems

· 7mo ago

Replying to

@jeremysiek@types.pl @krismicinski@types.pl I'm moving all of my classes to required code walks. Has the nice side effect of the fact that once you convince your students that the code walk grade doesn't suffer when you find a bug during it, it often turns into a design discussion and talking about debugging strategies. I think the students also feel like their hard work is more appreciated after they actually get to chat with faculty about it. Has worked wonderfully in undergrad compilers and grad distributed systems. Hard to scale past 40 students though

49

6

6

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

While there are many cases made for coding LLMs, one that keeps coming up that I literally don't understand is "it will save us so much time typing." I've seen a lot of people push back on this with very sensible points, like that most of software development is not the process of entering code into files, but planning, designing, coordinating with other teams, and so on.

But it occurs to me that for some of the folks hung up on the "less typing" point, maybe a lot of them (specifically those repeating this point) just never learned to touch-type, so text entry really is a bottleneck for them? Is that a plausible source of some of this?

Do they teach typing in schools anymore? I still occasionally encounter an upper-level CS or SE students who is doing hunt-and-peck. I don't think it's taught in my kid's school, despite having a "computers" class (middle school). I was required to take a "keyboarding" class (i.e., typing) in middle school, though I actually learned earlier via Mario Teaches Typing (the only educational software I'm fully convinced works).

18

18

2

0

Colin Gordon @csgordon@discuss.systems

· 2mo ago

Replying to

@ricci@discuss.systems I think it's partly the scale that they're not equipped for, but really the systems thinking about downstream effects of that scale. When I did my last IRB training I was struck by the fact that the system assumes either individual interactions with researchers xor Internet surveys--- that any serious impact requires direct interaction or publication of private information. No part of the system --- requirements or training for IRB members --- is tuned to consider impacts across millions of people (though this is the kind of obvious thing I'd expect submitters to identify clearly). This, that Minnesota kernel bug incident... I mean it's entirely possibly to fuck up traffic for millions bad enough that an ambulance doesn't get there in time, or accidents are made significantly more likely.

4

0

0

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

There are so many random IT systems at work that I get email from, that it's increasingly hard to tell the difference between a legitimate university system and a predatory conference, with all these emails from things with names like unisci and scisys and catalysis and ....

11

0

2

0

Colin Gordon @csgordon@discuss.systems

· 7mo ago

In PL we spend a lot of time thinking about how to ensure that type systems or program analysis tools are sound: that they only make valid predictions about code's behavior. (Or at least, are sound with a few explicitly identified exceptions like reflection.) But sometimes we get it wrong. Or sometimes we do get it right, but only after trying something more obvious that seems like it should be right, but turns out to be wrong. Or we get it right in theory, but there's an extra wrinkle in the implementation that wasn't obvious but affects soundness. The UNSOUND workshop colocated with ECOOP in Brussels this summer is looking for talk proposals around these and other related topics. If you think you have something interesting to talk about, please submit a talk proposal! The workshop is pretty low-key, I had a great time attending in 2024 (it's biannual).
https://2026.ecoop.org/home/unsound-2026

20

2

20

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

Do we sometimes ask computers today to do things that are genuinely beyond what those older machines could do? Sure, even focusing on typical consumer applications. Games are a big one. But I'm not talking about asking these machines to do anything new; I'm talking about using them for things *we already know they're very capable of doing*, not just in principle but because we've already used them that way! While I'm eager for the next AI winter, I have to wonder if prolonged pressure on RAM prices might finally push folks (companies, really) building consumer software to think "hmm, we should make sure this still runs on some machines with limited specs." 7/7(?)

8

0

2

0

Colin Gordon @csgordon@discuss.systems

· 6mo ago

I am extremely tempted to reorient the assignments in my fall software testing course around testing the leaked Claude Code source... give students something substantial to test and indirectly drive home why they shouldn't vibe code...
@jonny@neuromatch.social

neuromatch.social

jonny (nonvenomous): "OK i can't focus on work and keep looking at this…" - neurospace.live

7

0

2

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

Overall this was interesting, but ultimately disappointing. The G4 Hardware *still works*. Well. After 20 years. It has actual removable memory, so I could bump it to the hardware's 2GB RAM, replace the old drive, and keep using it for a long time, in principle. It's still actually more powerful than many recent Chromebooks. In fact was so much more powerful than the Pentium III (256MB RAM) I initially played StarCraft and Diablo II on that I barely knew what to do with it. Needless to say, I did plenty of research on the Internet back then; wrote, compiled, and tested tremendous amounts of software; wrote lots of word documents and made a few slide decks. Email. All the things we do now, without any issues at all. 5/n

6

1

2

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

OpenBSD doesn't support the 32-bit RPiZero (I haven't gone spelunking to find out if it ever did; the Zero 2 is 64-bit). So for the first time I installed the third major BSD, NetBSD. It's an SBC, so there's not really an installation. It just boots. X11 works. USB wifi over a hub works. There are only about a dozen processes running by the time you get to X. It was the first time since early 00s Slackware that 'top' didn't fill the screen. Also very responsive. Rust actually does support armv6, so I did eventually manage to compile my preferred editor (Helix), after 2 days of constantly restarting it because it kept overheating and crashing. I could have gone for better cooling, but I was also generally wary of running anything important off an SD card anyways. 4/n

5

3

2

0

Colin Gordon @csgordon@discuss.systems

· 7mo ago

Replying to

@lindsey@recurse.social @jeremysiek@types.pl @krismicinski@types.pl yeah... our first-year courses (~400 students) are trying a lightweight version of this with 10 minute chats, with random samples of students each week. so I think each student meets twice a term. It seems to be going well, but it's still a stretch even with an additional faculty member volunteering to help with these(!). The deeper material in later courses definitely needs more than 10 minutes.

6

4

0

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

@maxsnew @carloangiuli I think we're interleaving concerns about students at different levels. Nobody's assuming first-years are capable vim users. But we might expect familiarity and some competence with basic text editing affordances like those in, say, Word and Google Docs. Select, and cut/copy/paste? I think Carlo is saying he's not even seeing that in first-years (I haven't taught first-years in a long time). I was alluding to the fact that I'm coming to the realization that assuming basic touch-typing is not realistic, despite the fact that most of our students have been typing essays in a word processor for years before college, often many years. I was saying that at least later (closer to graduation?) students should have ideally gotten to the point where they can not only type proficiently, but be familiar with some preferred editor beyond its basic text editing capabilities --- even just for *navigating* code, but ideally to help them turn their thoughts into code faster. Of course this all falls into the "hidden curriculum" bucket, e.g. https://missing.csail.mit.edu/2026/development-environment/ and we need to figure out where to cover this stuff.... like I said, in my undergrad some of this was built into the systems programming course, but that's unusual

missing.csail.mit.edu

4

4

1

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

Nobody really maintains the mac PPC drivers for those machines in Linux, and distributions stopped maintaining macppc ports a surprisingly short time after apple switched to Intel chips. After some digging I managed to locate a mirror of an ancient copy of Yellow Dog Linux, but I was hoping to see how productive I could be today, not just boot a machine and declare victory, so I needed something modern. Turns out if you want to run a current-day OS on a G4, the only choices are NetBSD and OpenBSD, which both still (in 2026) maintain support for those machines. (FreeBSD discontinued all 32-bit support a number of years ago.) Options for the RPiZero are slightly less limited, as you can get various Debian derivatives (including Raspbian) for that hardware, even today. But my experience with those systems vs BSDs on newer hardware led me to focus on the BSDs first. 2/n

4

1

2

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

Some of this is reasonable economic forces and focusing limited human bandwidth. Nobody makes consumer PowerPC chips anymore, so of course new efforts are unlikely to target it (e.g., Rust). Fair enough. Similar factors come into play with 32-bit ARM application processors. But much of the software support *already exists*. The only thing breaking anything beyond games is the memory consumption of modern web browsers, and to a lesser extent office software. Why does opening a brand new browser instance, freshly installed, with no open tabs spike memory consumption by 2GB? I'm aware that there's more happening in today's web browsers than 20 years ago (I used to work on a JavaScript compiler). Also the switch to 64-bit adds some overhead vs the G4 (but my old *Opteron* was still blazing fast running Firefox under Solaris or Debian, with 4GB of RAM). Because Chrome is similarly bloated (or worse), everything built with Electron (VS Code, Obsidian, Zotero, countless other things) is also bloated. 6/n

4

1

2

0

Colin Gordon @csgordon@discuss.systems

· 7mo ago

Replying to

@jfdm@discuss.systems @lindsey@recurse.social @jeremysiek@types.pl @krismicinski@types.pl I've long had students do a form of this with their assignments, but the generated reports got "good" enough a year and a half or so ago that I spent more time waffling on whether something crosses the line plus basically arguing politely with offended students than I would just meeting with everyone. (I'm sure this balance point varies depending how exactly you set things up with the report, but I couldn't figure out a more effective setup.) Meeting with everyone has ended up more equal for students, less frustrating for me, and more positive (i.e., non-adversarial) for students. The tipping point also depends on enrollment.

5

2

0

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

@samgoree another thing I've been mulling over is comfort with editors, which is sort of a follow-on to touch-typing. I've shocked students by adding a method to every Java class in a file with a one-liner in vim. And of course, to be fair, adding a method to every class in a file by abusing sed-style search-and-replace both requires a deep comfort with syntax and existing program structure, and is objectively a bizarre way to express a conceptually structural change. So it's not exactly an obvious thing to do, even if it's common among long-term vim and emacs users. But when I watch students use their IDEs, even as seniors, I see them do things like use textual find to locate definitions, tabbing through dozens of call sites before hitting the declaration, instead of "just" using the IDE's built-in go-to-definition. To students who don't understand their IDE as anything more than a text editor with a compile&run button (I'm sure some working professionals are in this camp, too), doing complex structural changes quickly by any means must seem magical.

3

1

0

1

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

Installing OpenBSD on the G4 was just like on any other computer. Uneventful. (Beyond that installing OpenBSD always gives me vague Linux-from-Scratch vibes.) It booted. Needed a USB wifi, but that's it. Sticking to the basic window manager for light resource use, very snappy. The lack of modern browser and lack of Rust support were the main blockers for my personal longer-term use (see linked thread above, no binary packages for Firefox it Chrome variants b/c they need too much RAM for a native PPC build). 3/n

3

1

2

0

Colin Gordon @csgordon@discuss.systems

· 6mo ago

https://github.com/servo/servo/pull/43116
#Rust #FreeBSD #Servo

Port Servo to FreeBSD by nortti0 · Pull Request #43116 · servo/servo

Add the minimum amount of FreeBSD-specific code to Servo, where no platform-neutral fallback exists. Testing: I've succesfully built and run Servo on FreeBSD with these changes (and some fixes ...

3

0

2

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

@maxsnew awesome, congrats!

2

0

0

0

Colin Gordon @csgordon@discuss.systems

· 7mo ago

Replying to

Above was a screenshot of an email to me from GitHub Education, reading: To our educator community, We want to keep you informed about an upcoming update that will change how GitHub Copilot is packaged and managed for students. At GitHub, we believe the next generation of developers should have access to the latest industry technology. That commitment is central to GitHub Education, and it’s why verified students can use GitHub Copilot for free. Today, nearly two million students rely on Copilot to build, learn, and explore new ideas. As Copilot continues to evolve quickly—with new capabilities, models, and experiences shipping at a rapid pace—and as student usage continues to grow globally, we are making some adjustments to ensure we can continue to provide GitHub Copilot access to students worldwide for free. We support a global community of students and teachers across thousands of universities and dozens of time zones, so we’re being intentional about how we roll out changes, starting small and validating what works. What’s changing for students Starting today, March 12, 2026, students’ Copilot access will be managed under a new GitHub Copilot Student plan, alongside their existing GitHub Education benefits. Their academic verification status will not change, and there is nothing students need to do to continue using Copilot. They will see that they are on the GitHub Copilot Student plan in the UI; existing premium request unit (PRU) entitlements will remain unchanged. As part of this transition, however, some premium models—including GPT-5.4, and Claude Opus and Sonnet—will no longer be available for self-selection under the student plan. We know this will be disappointing, but we’re making this change so we can provide a sustainable offering and keep Copilot free and accessible for millions of students around the world. Ensuring long-term, sustainable access for the entire student community means making difficult tradeoffs today. That said, through Auto mode, students will continue to have access to a powerful set of models from providers such as OpenAI, Anthropic, and Google. We'll keep adding new models and expanding the intelligence that helps match the right model to your task and workflow. We support a global community of students across thousands of universities and dozens of time zones, so we’re being intentional about how we roll out changes. Over the coming weeks, some students may see additional adjustments to available models or usage limits on certain features—the specifics of which we'll be testing with student feedback. We will make sure to share full details and timelines before we ship broader changes. What’s not changing GitHub Copilot remains free for verified students as part of GitHub Education. Verified educators will continue to receive complimentary access to GitHub Copilot Pro.

3

0

1

0

Colin Gordon @csgordon@discuss.systems

· 7mo ago

Replying to

@jbigham@hci.social @lindsey@recurse.social this is a really bizarre take on what happens in other disciplines. CS PhDs are usually paid stipends because there is (was?) a massive array of federal and industrial organizations making CS a financial priority. This simply doesn't exist for humanities; there are fewer sources with less money each. They're paid more than many other STEM fields because we needed to shrink the salary opportunity-cost of pursuing a PhD, and because of the abundant funding sources we could. CS PhD students often do the same work as others who are paid less. Complexity theory and logic research happens in CS, math, and philosophy; why are they paid differently? Same with NLP research in CS vs linguistics. Some of the same work, published in the same venues. Digital humanities and STS researchers, including grad students, write plenty of code. I had a faculty friend in the political science department here who left for a position with almost double her salary. Which was possible because her research day to day, including during her PhD, was mostly coding(!) (data analysis of information to identify war crimes, which seems more important than most CS PhD work, my own included). And more broadly, a PhD is fundamentally an apprenticeship, learning research by doing, so there's not really a meaningful distinction between learning how to do research and doing research.

2

2

0

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

@carloangiuli yes definitely, also something I've been pondering https://discuss.systems/@csgordon/116417422123280049

discuss.systems

1

0

0

0

Colin Gordon @csgordon@discuss.systems

· 5mo ago

Replying to

@regehr @pkhuong wtf???

1

0

0

0

Colin Gordon @csgordon@discuss.systems

· 6mo ago

Ugh, no!
@lu_leipzig@troet.cafe

1

0

1

0

Colin Gordon @csgordon@discuss.systems

· 7mo ago

Replying to

@gannimo congratulations!

1

0

0

0

Colin Gordon @csgordon@discuss.systems

· 14mo ago

Replying to

@regehr@mastodon.social my head wants to explode, LLMs are legitimately not good at assessing correctness or correspondence between code and natural language... I have the privilege of being able to just not submit to a venue that asks LLMs to assess correctness of submissions, but that's going to be a mess for junior people if they actually do that

3

1

0

0

Colin Gordon @csgordon@discuss.systems

· 33mo ago

My PhD student is running a research study evaluating the quality of automatically generated code comments. We are looking for participants comfortable with English Python documentation to judge a number of comments on several quality measures. If you’re interested, please take a look at the first page of the survey https://drexel.qualtrics.com/jfe/form/SV_3PCMGre95GTIyy2 for more details and to participate if you like. Thanks!

🔁 boosts to get the word out are appreciated!
#Python #programming

drexel.qualtrics.com

Comment Quality Evaluation

A study of the quality of human and automatically-generated comments.

10

0

28

0

Colin Gordon @csgordon@discuss.systems

· 9mo ago

Replying to

@joey@mathstodon.xyz @wilbowma@types.pl the only way to see the summary is with premium. At most schools, you can look up a paper title in your library's search and if you have access through your institution, the result will have a link that sorts out whatever institutional proxy is needed to view it with the institutional access. That's the only thing that works reliably for me

1

0

0

0

Colin Gordon @csgordon@discuss.systems

· 33mo ago

Replying to

Ich soll sagen, das ich einen Artikel (nur eins) gefunden habe, der vier (!) Beispiele hat. https://www.degruyter.com/document/doi/10.1524/auto.52.2.A1.34758/html Hoffman und Langes sehr interessantes Buch hat keine Beispiele von Formulare mit deutsche Beschreibungen. Ich kenne keine andere möglichen Quellen.

0

2

0

0

Colin Gordon @csgordon@discuss.systems

· 33mo ago

Replying to

Französischen Referenzen wären auch hilfreich, obwohl mein Französisch nicht besonders gut ist

0

0

0

0

Colin Gordon @csgordon@discuss.systems

· 6mo ago

@dysfun@social.treehouse.systems totally, it's a consequence of the system design.

I guess maybe I'm trying to suggest that perhaps it's a suboptimal design. I realize that on the modern web there's only so much you can do to reign in JavaScript memory consumption, but I'm starting to wonder how far we *could* go, on both the browser and serving side. I've been fiddling with @jonmsterling@mathstodon.xyz's Forester system lately, which is lovely, and a stark reminder how good things can be with fairly things shipped to clients.

0

0

1

0

Colin Gordon @csgordon@discuss.systems

· 2mo ago

It's no secret that I'm deeply opposed to LLM-based technology in almost every context, but the very idea of using these things to triage 911 (US emergency number) calls should notify absolutely everyone, *including* their proponents in other contexts. Handling 911 calls is a textbook safety-critical system: if something goes wrong, people are likely to die, in addition to other outcomes (injury). I called my pharmacy yesterday, and of course got a voice recognition system. I, a native English speaker (of American English) with a roughly median US accent, said I was calling to ask a pharmacist about prescription drug interactions. I was routed to the menu for the status of my prescriptions, not the path to talk to a pharmacist. This is a for profit national chain that, while I'm sure they want to save money, also certainly recognizes that phone systems are also part of them *making* money, so have a clear incentive for these things to work well, tied to their primary business function (making money). And it can't handle someone who's accent is almost certainly around the median of their training data calling for one of the most common reasons anyone calls a pharmacy. The only reason anyone would replace https://masto.deoan.org/@neurovagrant/116981820059237731

masto.deoan.org

0

0

0

0

Colin Gordon @csgordon@discuss.systems

· 4mo ago

Replying to

@mwl@io.mwl.io maybe your machine needs a kick with efibootmgr? https://man.freebsd.org/cgi/man.cgi?query=efibootmgr&apropos=0&sektion=8&manpath=FreeBSD%2B15.0-RELEASE&format=html I mean, it *shouldn't* need you to run efibootmgr yourself if you're putting it in the standard location on an EFI partition, but I have had to do this a couple times on machines with flaky firmware

The FreeBSD Project

0

0

0

0