Elektrine
EN
Log in Register
Paige Chat Timeline Communities Gallery Videos Email DNS VPN Uptime Kairo
Back to Timeline
Remote

Colin Gordon

@csgordon@discuss.systems
  • Open on discuss.systems

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.

:freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

495 Followers
1478 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/

Posts

Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Jul 25, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
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
0
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Jul 22, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @ricci@discuss.systems
@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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · May 15, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @mwl@io.mwl.io
@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
0
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 30, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @maxsnew@types.pl
@maxsnew awesome, congrats!
2
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 21, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 17, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @maxsnew@types.pl
@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
4
4
1
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 17, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @carloangiuli@mathstodon.xyz
@carloangiuli yes definitely, also something I've been pondering https://discuss.systems/@csgordon/116417422123280049
1
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 17, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @samgoree@hci.social
@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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 17, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @regehr@mastodon.social
@regehr @pkhuong wtf???
1
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 17, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
1
2
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

Related to this post, I've really been wondering about this, and e-waste, and planned obsolescence for a while, and trying things I never found time to write up.... guess I'll dump my thoughts here for now.
@csgordon@discuss.systems

In 2023 I started trying various old hardware I have laying around, including a first generation (pre-ordered!) raspberry pi zero, and the G4 (not M4) PowerBook I took to college in 2004. Both 32-bit machines with 512MB of RAM.
1/n

10
1
2
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 10, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

@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.

social.treehouse.systems

gaytabase (@dysfun@treehouse.systems) - Treehouse Mastodon

0
0
1
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 02, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

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

3
0
2
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Apr 01, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

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

7
0
2
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 28, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

Ugh, no!
@lu_leipzig@troet.cafe

troet.cafe

Prüfungsphasen-Recovery-Lu 🤕: „@HaTetsu@mastodon.com.pl @davidgerard@circumstanc…“ - troet.cafe - M

1
0
1
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

Looks like the underpricing of these generative "AI" tools to get people hooked might be under strain... Normally verified students get access to all kinds of expensive goodies because companies are hoping to get the students to drive future business by setting their expectations for professional tools.

8
2
2
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 08, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @jbigham@hci.social
@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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 08, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @gannimo@infosec.exchange
@gannimo congratulations!
1
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 05, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @jfdm@discuss.systems
@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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 05, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @lindsey@recurse.social
@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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Mar 05, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @jeremysiek@types.pl
@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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Feb 12, 2026
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Dec 17, 2025
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @joey@mathstodon.xyz
@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
0
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Jul 31, 2025
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @regehr@mastodon.social
@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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Jan 03, 2024
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

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

10
0
28
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Dec 27, 2023
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
Französischen Referenzen wären auch hilfreich, obwohl mein Französisch nicht besonders gut ist
0
0
0
0
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Dec 27, 2023
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems
Replying to @csgordon@discuss.systems
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
Open post
csgordon
Colin Gordon @csgordon@discuss.systems · Dec 21, 2023
Colin Gordon
@csgordon@discuss.systems

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. :freebsd_logo: :debian: :openbsd: :clang: :csharp: :racket: :rust:

discuss.systems

Ich habe eine Referenzanfrage: kennt jemand ein Buch oder Artikel über LTL (Lineare Temporale Logik) auf Deutsch, das viele Beispiele für Übersetzungen vom Deutsch ins LTL enthält? Hofmann und Langes Buch enthält natürlich keine Beispiele, nur Mathematik 🙃

(Ich verstehe LTL ganz gut, ich suche nach Beispiele auf Deutsch.)

2
2
4
0

Remote instance

discuss.systems
Open on original server

Media

313k7r1n3
Elektrine

Tor hidden service

elekhj7afj4qnrr4yd3bkzslsyo5jgfxw3orgjkhlcxifueodybyiiad.onion

Platform

  • Email
  • Chat
  • Timeline
  • Communities
  • VPN
  • DNS

Company

  • About
  • Contact
  • FAQ

Legal

  • Terms of Service
  • Privacy Policy
  • Warrant Canary
  • Lite (no JS)
  • VPN Policy
  • Source code

Support

  • support@elektrine.com
  • Report Security Issue
Mail client setup IMAP mail.elektrine.com:993 POP3 mail.elektrine.com:995 SMTP mail.elektrine.com:465
© 2026 Elektrine. All rights reserved. Server: 22:34:52 UTC