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:

Posts

Post #4094658
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 nativ...
Post #2162710
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.)
Post #2162707
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
Post #1809100
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&#39;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&#39;s an extra w...
Post #1513708
@dysfun totally, it&#39;s a consequence of the system design. I guess maybe I&#39;m trying to suggest that perhaps it&#39;s a suboptimal design. I realize that on the modern web there&#39;s only so much you can do to reign in JavaScript memory consumption, but I&#39;m starting to wonder how far we *could* go, on both the browser and serving side. I&#39;ve been fiddling with @jonmsterling&#39;s Forester system lately, which is lovely, and a stark reminder how good thi...
Post #1513707
Related to this post, I&#39;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&#39;ll dump my thoughts here for now. https://discuss.systems/@csgordon/116382050700479908 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...
Post #1513705
There are so many random IT systems at work that I get email from, that it&#39;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 ....
Post #1467650
While there are many cases made for coding LLMs, one that keeps coming up that I literally don&#39;t understand is &quot;it will save us so much time typing.&quot; I&#39;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 &quot;less typing&qu...
Post #1000188
Looks like the underpricing of these generative &quot;AI&quot; 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.
Post #1000185
Ugh, no! https://troet.cafe/@lu_leipzig/116308565177870577
Post #1000184
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&#39;t vibe code... https://neuromatch.social/@jonny/116326861737478342
Post #1000182
https://github.com/servo/servo/pull/43116 #Rust #FreeBSD #Servo