Pinned toot

My name is Rob. I grew up a military brat, but my family is generally from the midwestern US.

I was a software engineer for about a decade, including a ~5-year stint at Square (the payments processor). I made the move to academia about 4 years ago, and I am currently working on a PhD studying programming languages at Purdue with Ben Delaware.

I'm an avid reader in general, and like science fiction in particular. I like to fence, although I do it less than I used to. I play violin and piano equally terribly, and I have a beautiful family who is forced to listen.

Entering the US public domain in 2023: Fritz Lang's silent film science-fiction classic *Metropolis*.

More info behind window 6 of our advent-style countdown calendar for works entering the #publicdomain on Jan 1st: #PDin2023 #film #metropolis

This modified version of the famous ‘turn #chatGPT into a pretend Linux system’ prompt is also my prototype for a product that will sell millions.

If there are no questions after a talk the session chair should just generate some with ChatGPT.

now ChatGPT seems really impressive and all but you have to remember that you can be tricked into thinking a rock has feelings by drawing a cute face on it

How would you use Hoare logic to verify an API migration did not introduce new behaviors? If the API spec allows multiple implementation choices, you need to reason about relational liveness over nondeterministic executions, but relational Hoare logics don't support this kind of reasoning... until now!

Check out my APLAS talk "RHLE: Modular Deductive Verification of Relational ∀∃ Properties" Monday at 1:30p.

🗣️​ Talk abstract:

📄​ Preprint:

In Auckland with like 6 hours to kill. Suggestions?

This week, LastPass, and its parent company GoTo, both published blog posts about their recent data breach:

But if you search for GoTo's blog post in Google, you won't find it, because GoTo hid its breach notice from search engines using "noindex" code.

Pong is 50 years old today.

Little known fact: Pong has no code. Pong doesn't even have a microprocessor. Al Alcorn hardwired the game with transistor-to-transistor logic. (See Henry Lowood:

Hi, we're a group called PhilTel aiming to install free-to-use #payphones in #Philadelphia. We are having an install party at @iffybooks on December 17th where we will install our first phone (more info here,!

We will also be distributing a zine that explains the project and some of the interesting things you can do with the phone.

For more info, check out


*shuts down laptop*
I think that's enough internet for today

*picks up phone*
Let's see what the pocket sized internet is doing

As an app-only walled garden, Hive Social is not a part of the World Wide Web in any meaningful sense. Anyone letting it get their hooks into them is making a familiar and terrible mistake. We've been here before. Don't let it happen again.

Most of SPLASH 2022 is less than one week away, but the virtual talks at OOPSLA are happening *tomorrow* (or today, depending on your timezone)! Join us at V-OOPSLA and watch some exciting talks from your home/office!

@channingwalton The most mind bending thing about borrowing in Rust to anyone coming from Haskell and friends is that `Fn(A) -> A` and `Fn(&mut A)` mean exactly the same thing as far as immutability goes.

@eniko @thephd We’ve recently been rewriting the Swift parser, and have some opinions on how to do this well: good parser primitives (“expect this”, “match this”, “don’t go beyond that”, etc.), no diagnostics from parsing itself (represent all issues as missing/unexpected nodes in the tree), and handle diagnostics in a post-pass. The result is really nice and is easy to extend to@new grammar terms. See

Them: Are you going to be part of the problem or part of the solu—

Me: Oh problem, definitely

Them: That wasn’t…it was a rhetorica—

Me: I have some ideas on how to make the problem even funnier than it is

Show thread
Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.