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

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