chris martens

go slowly and quietly, and look deep

pronouns: any/they
default location: Boston, MA
unfinished personal website: https://chrisamaphone.hyperkind.org/
dorky professor website: https://khoury.northeastern.edu/~cmartens/

Public Key

npub1yp3qerlleys6mvvc4488qfnnwy732sa3ck0meq7yuefzy6nzm7jqxsun2n

NIP-05 Address

chrisamaphone_at_hci.social@momostr.pink

Profile Code

nprofile1qqszqcsv3llujgddkxv26nnsyeehz0g4gwcut8aus0zwv53zdf3dlfqpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dswrwv88

Publishing to

relay.damus.io

nos.lol

Author Public Key

npub1yp3qerlleys6mvvc4488qfnnwy732sa3ck0meq7yuefzy6nzm7jqxsun2n

Show more details

Last Notes

2026-10-31 14:08:29 UTC

- reply

possible exceptions:
- "protraction", which suggests a deliberate lengthening. but i feel like this is still most used derogatorily, as in something going on for too long.
- "lentitude", because it's uncommon and so seemingly more neutral to my ear, and because it reminds me of "lento" tempo in music, a context where slowness is prescribed

2026-10-31 14:02:04 UTC

i'm thinking about the ways in which "working really fast with a lot of output" asserts itself as a cultural value and how hard it can be to communicate the value of slowness as something aligned with dedication and investment in a project. it feels like [english] language gets in the way here: all the synonyms i can find for slowness either seem to connote laziness, indifference, disinclination to work; or complete stoppage of progress.

2026-10-30 21:59:51 UTC

apparently it's become controversial to say that i think there is interesting and important PL research to do without ever touching an LLM, and the burden is on *me* to prove it rather than on others to tell me why everything they cared about three years ago stopped mattering.

2026-10-25 15:30:48 UTC

we gotta talk about how to audit mechanized proofs. lots of us have been saying this since the early days of artifact evaluation but no one listened 🤷🏻

2026-10-03 14:27:56 UTC

PL 🤝 bookmaking
tinkering with different ways to implement binding, signatures, and closures

2026-09-25 15:48:07 UTC

- reply

(continuing 🧵:) a colleague has informed me that the video of my PLATEAU talk ("is truth future-proof? on the possible futures of mechanized proof") is available now: https://www.youtube.com/watch?v=teevzT1Arrw
(him: "i like how you start out by saying, 'there are many threats to truth.'"
me, mortified: "did i really say that??")

2026-09-19 20:07:01 UTC

pen and paper as low resource computing platform

2026-09-12 00:51:46 UTC

in light of recent mechanized math news, i want to re-promote the paper my colleagues and i published earlier this year about the nature of mathematical knowledge represented by mechanized proofs: https://khoury.northeastern.edu/~cmartens/papers/plateau26-itfp.pdf
especially the "convincing" and "explaining" distinction between modes of use. our framing was about proof longevity & archival, but this distinction also pertains to how we think about new mechanizations in real time, what social functions they actually serve

2026-09-11 19:03:17 UTC

folks working in theoretical PL or logic/math-adjacent CS: if someone in your department were teaching a "research methods" class and wanted you to suggest some readings related to the methods used in your field, what would you send them?
i've had lots of interesting conversations about this, but what's been written and published? (i'm also interested in your opinions even if they're not written down in papers, but secondarily.)

2026-09-09 10:51:14 UTC

i'm really unimpressed with how quickly academics seem inclined to throw *ourselves* under the bus with this "ai product supremacy is inevitable" bullshit. you realize this propaganda is part of the active political mission (which has been made quite explicit by certain people in power) to destroy public perception of universities and end the possibility of people like us having the lives and careers we have, right?? we don't have to lie down and take it.

2026-08-25 12:09:11 UTC

few things make me sadder about genAI use than people who think they "can't draw" making images with it that they use in their creative work.
if you are in that category and we ever find ourselves sharing physical space, let this represent my personal offer to coach you on sketching simple shapes on paper or in free digital tools that you can use in these circumstances. it's slower and the results might be less "polished", but it's a skill you can develop and use for your whole life

2026-08-23 22:15:23 UTC

- reply

everyone i know who submitted something seems to have been asked to review. at least they seem to be distributing the load somewhat fairly?

2026-08-19 23:54:38 UTC

alright i just finished it and my new hot take is that Artemis is Andy Weir's best novel

2026-08-16 02:04:08 UTC

what else exists in the genre of "roxanne but it's just rocks"

2026-07-03 14:24:12 UTC

- reply

okay i love everything about this. (tag yourself i'm mathbat)
https://storage.googleapis.com/hci-social-storage/media_attachments/files/116/856/486/657/042/667/original/d8100f7d2aae7fa9.png

2026-07-03 13:49:24 UTC

is... someone out there using these *not* as a joke?
https://storage.googleapis.com/hci-social-storage/media_attachments/files/116/856/350/338/373/498/original/ccf00e780ee6f8be.png

2026-07-03 02:09:48 UTC

- reply

wdym by statements? i read your replies to azul and i'm still confused. i assumed you meant imperative computation like array assignment or for loops or something, and i was thinking that any "function" in an imperative language is basically a way to "compute a statement" in this sense. but maybe you mean the thing i would call a declaration or definition?

2026-06-23 20:27:49 UTC

my decision to stay fluent in a programming language with a stable legacy implementation of a 1997 formal definition feels pretty good these days

2026-06-19 16:05:15 UTC

who's out there using proof assistants in conjunction with disability assistive tools (screen readers, voice control, custom input devices, etc)? i want to know what your setup and experience is like. (boosts welcome; right now this is just a curiosity and not a research project)

2026-06-17 17:58:47 UTC

what's it called when you reparse a string of letters as different sequences of words like standoffish / stand of fish, or who remembers / whore members? eggcorn is close but i think that's more phonetic

2026-06-05 17:28:04 UTC

fyi when the instructions for something include "enjoy!", most things still seem to work even if you skip that step. this has saved me a lot of unnecessary effort

2026-05-19 22:41:33 UTC

TIL david foster wallace's first novel was an adaptation of his senior thesis on modal logic

2026-05-12 14:32:49 UTC

what are some examples of physical crafting that *feel* really good to you in the process (regardless of how much you like the end result)? alternatively, where the end result is something that you really enjoy on a sensory level?

2026-05-05 12:49:22 UTC

may the fifth be wifth you

2026-04-28 20:39:40 UTC

used to be "make a little logo for your project for a token amount of extra credit" was a way to give students permission to do a tiny bit of low effort art as a treat. everyone knew it could just be bad and that would be part of the charm; it would still connect you in a personal way to your creative efforts. i forgot this doesn't work anymore, and i'm sad about it.

2026-03-31 18:29:11 UTC

- reply

arguably we should also want archival programming languages more generally. sometimes, a language whose features cease to evolve is called "dead". but perhaps we should reserve "dead" for languages whose programs no longer run, and use "archival" for those whose implementations are maintained while their feature sets remain stable (thx @npub1d2t…dzc9 for planting this lexical seed in my head)

2026-03-31 18:12:04 UTC

- reply

thanks! i'm interested in hearing what you think if you have a chance to read further on

2026-03-31 18:00:30 UTC

re: https://hci.social/@chrisamaphone/116325060049701188
taking off my "impartial observer" hat for a moment (and so breaking out of the thread), one opinion i've started solidifying is that we need stable (or one might say "archival") proof languages, alongside those that actively evolve. a big motivation for me is to develop teaching materials that still run in a decade (Explaining), but i think there are good Convincing-aligned reasons to want this as well.
#note1fl3…fjn5

2026-03-31 17:52:33 UTC

- reply

PLATEAU is a workshop, so this paper is mostly a discussion starter that gestures towards possible projects (we aren't describing a new solution or advocating for a particular agenda). i really want to hear from more folks about your answers to the discussion questions at the end, or any other feedback!

2026-03-31 17:49:13 UTC

- reply

people shouted out in the talk include [@ionchy](https://types.pl/@ionchy ) (for their lovely reproduction of Reynolds' "types, abstraction, and parametric polymorphism"), @npub14a5…9fse for his posts about Agda as communication tool, and @npub1had…j35h for letting me ask annoying questions about his Lean projects :)

2026-03-31 17:46:52 UTC

- reply

another line of thought that emerged (and appears more significantly in the talk slides than in the paper) is how the desire to future-proof proofs participates in the broader human project of cultural artifact archival, alongside the history of media forms like film, games, net art, etc. and their respective challenges and changes to the technical needs of archives.
also, how stewardship matters. the work of re-transcribing and re-situating old work is how we express our care for its value

2026-03-31 17:39:04 UTC

- reply

one of the outcomes of this work i want to highlight is the observation that not everyone mechanizes proofs for the same reasons. there are motivations that derive from:
- *Convincing*: wanting to improve confidence in results as objects of study scale in complexity;
- *Explaining*: wanting to improve precision and clarity in definitions, communicate ideas, and identify reusable abstractions.
a lot of talking past each other can happen when we conflate these purposes

2026-03-31 17:33:25 UTC

new from me, @npub1t7d…zxtp , [@cxli](https://scholar.social/@cxli ) , and Elan Semenova: "Is truth future-proof? On the possible futures of mechanized proof". contains provocations, philosophical framings, and accounts of current practices in light of the idea that mechanized proofs contain mathematical knowledge that we might want to persist across future generations.
preprint: https://khoury.northeastern.edu/~cmartens/papers/plateau26-itfp.pdf
presented at PLATEAU a few weeks ago. slides: https://khoury.northeastern.edu/~cmartens/talks/plateau-itfp-talk-slides.pdf

2026-03-29 16:41:10 UTC

someone please tell me i am not the only one who made it to full adulthood before realizing that "20 thousand leagues" is not a reasonable distance for something to be towards the center of the earth from the surface of the ocean and that in fact it was the distance *traveled* (under the sea) by the nautilus in the eponymous tale

2026-03-22 15:10:33 UTC

current progress on becoming [@justinefrank](https://types.pl/@justinefrank )
https://storage.googleapis.com/hci-social-storage/media_attachments/files/116/273/446/255/652/479/original/5635e02e5ed5ddcb.mp4

2026-02-06 01:13:48 UTC

thank you for making this @npub1jxf…0dxv
https://storage.googleapis.com/hci-social-storage/media_attachments/files/116/021/023/581/481/598/original/86bed2e6b3c45ca8.png

2026-01-07 04:16:35 UTC

believe it or not this is two cats
https://storage.googleapis.com/hci-social-storage/media_attachments/files/115/851/871/665/760/811/original/a54c03f0ce3f4236.jpeg

2025-12-31 18:16:49 UTC

- reply

what are examples of items you are usually happy to receive for free?

2025-12-31 18:15:25 UTC

thinking about a spectrum defined by the endpoints “corporate conference swag” and “party favors.” i like the concept of making copies of items with esoteric symbols and giving them to people. i don’t like the concept of proliferating poorly made stuff that will end up in the trash or cluttering a drawer

2025-12-29 22:24:43 UTC

somewhere a crow who studies human behavior is patiently explaining to their colleagues that actually humans are somewhat sophisticated primates who even seem to understand language to the level of a young hatchling, not just imitating sounds but even using them in appropriate contexts

2025-12-04 13:43:23 UTC

i know this is a weird thing to say as a PL researcher, but i kind of like designing programming languages

2025-11-30 01:05:18 UTC

which of the following have you walked across? (this is supposed to be a multiple choice poll, hopefully it works)

2025-11-27 02:09:19 UTC

how on earth does someone make a podcast interviewing almost 60 people in programming language research in the last five years and only talk to 1-2 women

2025-11-18 00:07:55 UTC

tuple

2025-11-16 13:30:25 UTC

a generation of people enjoying the prosocial power of the internet before the age of slop: lets put all this cool stuff online for free! :)
emboldened capitalists in the 2010s-20s: wow look at all the stuff these suckers put online for free. I wonder what’s the worst possible thing we could do with it

2025-11-01 18:18:07 UTC

- reply

(I just deleted a toot that made no sense because I made an incorrect assumption about the argument in the video without watching it, whoops.)
I recently spent some time hearing Chris Barker, a famous enough linguist to have a Wikipedia page, try to convince PL people that natural language and PLs are “the same thing”, which I didn’t fully buy, but he had good takes on a lot of the topics in your thread

2025-10-30 12:43:46 UTC

Boston MFA restores ownership of and repurchases historic ceramic pieces created by enslaved artist David Drake to his known descendants: https://www.mfa.org/press-release/david-drake-ownership-resolution
i find this both important and uplifting from within a milieu of seeing artist labor/agency, racial justice, and historical preservation discarded everywhere i look

2025-10-21 16:22:02 UTC

when writing about mathematically esoteric concepts for workaday programmers interested in better understanding foundations of computing, there’s a tricky line to walk between “telling convenient but dangerous lies” and “failing to meet your audience where they’re starting from.”
do you have examples of material (blog posts, course notes, video, toot threads, etc) that you think does a good job at this? let’s give some positive attention to people doing the work. self promotion encouraged!

2025-10-17 21:24:26 UTC

- reply

if there were, hypothetically, a small website listing some logic/types-interested french faculty who are open to hosting a student (maybe with some metadata like research interests and websites), i’d be happy to circulate it to get seen by more people. but i also understand if that’s not necessarily desired :)

2025-10-17 21:20:36 UTC

- reply

that makes sense. i guess the coordination mostly takes place by word of mouth between french and usian faculty colleagues then? (that would be similar to what i did in grad school when i worked with dale and kaustuv at palaiseau for a summer.)

2025-10-17 19:37:54 UTC

- reply

do you know more about how this works? Does a student get matched with a particular mentor or program, or is there a way for them to identify someone in advance that they want to work with?

2025-09-20 00:39:38 UTC

went to a #bostodon meetup organized by @npub16z4…f7c7 . the tiny people in my phone exist in real life apparently?!

2025-09-19 12:31:22 UTC

pagemelt made a 3 minute explainer on RSS feeds, perhaps to share with the three minute video enjoying people in your life who are curious about alternatives to algorithmic media feeds https://youtube.com/shorts/Q8iLKjO0Z1A?si=8rchRwuWZRmBL6Pr

2025-09-03 12:38:07 UTC

self mollifying code

2025-08-31 18:21:39 UTC

- reply

idk it feels suburban to me! i am no expert though

2025-08-31 17:26:40 UTC

i’m at a suburban shopping centre doing some top rope climbing and just noticed there’s a conveyor belt sushi place… so 90s…..

2025-08-30 01:18:06 UTC

- reply

it’s ALMOST over the garden wall season but NOT YET

2025-08-30 01:16:07 UTC

- reply

need not be anything released recently

2025-08-30 01:15:42 UTC

what’s a good movie/game/book/show you’ve [appropriate verb]ed lately

2025-08-27 15:01:32 UTC

- reply

(2/2) but of course lots of good ideas about language design have been realized in the meantime and its age means it doesn’t benefit from those. i’m open to being persuaded that something else is more suitable to my goals, which are: 1. rapid prototyping of small, easy-to-understand reference implementations and 2. eventual adaptation of prototypes into performant implementations.

2025-08-27 14:56:42 UTC

does anyone want to talk me out of using Standard ML for a (functional) language implementation project? i favor it for a) stability (hasn’t changed in a long time and shows no signs of changing soon), b) easy (for me) to use, has standard nice typed FP features like pattern matching & inductive definitions, no complicated package manager/build tool story; c) performance: easy to reason about memory usage; performant compilers exist. 1/(2?)

2025-08-25 00:38:52 UTC

some youtube thinkpiece i watched weeks ago made this observation: the imagery of lofi girl lets us imagine being at peace and focused while working, to remember that productivity isn’t inherently antagonistic, hurried, exhausting, despite what many of us experience day to day

2025-08-22 13:03:51 UTC

how come cats get to sit in chairs all day and no one tells *them* it’s wrecking their bodies

2025-08-15 16:38:41 UTC

phd advisors: have any of you made reading lists of papers you want all your students to be familiar with? or maybe you build these for individual new students? does your group have a “canon”?

2025-08-12 02:07:39 UTC

- reply

i went to my local one and there were like 200 people… very cool but intimidating when it comes to introducing myself. Need to go a few more times to start recognizing regulars :)

2025-08-11 22:07:20 UTC

it’s common to wonder how to make friends as an adult in the area where you live, but i’m curious about flipping this on it’s head: how and where would someone find *you* in a disposition open to making a friend? in what situations do you welcome an introduction to a stranger?

2025-08-08 22:57:47 UTC

i’m participating in a local bouldering comp tomorrow, my first! wish me good climbing!

2025-08-08 17:28:57 UTC

- reply

huh, my preferences are opposite to the majority in both cases. it’s weird how other brains are not my brain

2025-08-08 01:41:28 UTC

apparently USA Climbing banned trans women from competing last month to comply with executive transphobia. this article does a good job covering it:
https://www.climbing.com/news/usa-climbing-bans-trans-women/

2025-08-07 15:24:25 UTC

- reply

have any of you (#adhd pals?) hired a personal admin to help with things like deadlines and bookings and phone calls? or tried and found it more trouble than it’s worth? or have any recommendations for where to look? (maybe someone on here wants to get hired for this kind of thing???)

2025-08-07 15:21:10 UTC

- reply

i remember on at least some occasions university staff offering this service (i think even when i was a grad student i had access to this service??) but afaik it is not a thing here. I mean also faculty used to be assigned individual “admin assistants” so a lot has changed

2025-08-07 15:17:49 UTC

I understand why some people don’t like them but i really wish i had a travel agent to help me manage academic travel

2025-08-07 01:40:59 UTC

- reply

okay what about

2025-08-06 01:36:43 UTC

2025-08-04 17:39:00 UTC

- reply

there are a lot of examples in a book I have that I will try to take some pictures of next time i’m near it. but it’s a declarative graph structure rather than sequential blocks of instructions. I wanna compile from one to the other (or both directions even???)

2025-08-04 17:37:44 UTC

- reply

btw my favorite notation for crochet is (maybe a variation on) stitch maps: https://stitch-maps.com/

2025-08-04 17:37:16 UTC

- reply

yeah that’s fair, often yarn that looks pretty feels bad and it’s hard to tell that from a picture

2025-08-04 17:33:24 UTC

- reply

what kind of yarn is this? I like it!

2025-08-04 17:28:05 UTC

- reply

what funky threading combinators? I don’t think I’ve come across these

2025-08-04 17:26:33 UTC

- reply

wouldn’t single crochet be push, yo, pull, yo, pull 2?
the thing you describe here sounds like what i learned as a slip stitch (and what you were describing as slip stitch earlier sounded like there was an implied extra chain or something, I didn’t quite follow)

2025-07-29 16:04:44 UTC

- reply

i’ve historically avoided getting interested in the lower level aspects of computing because i’m allergic to constraints that feel arbitrary, but more and more lately i’m appreciating how the PL ideas often seen as “maximally theoretical” have surprising and deep connections to low level, resource-minimal execution models

2025-07-29 15:39:10 UTC

- reply

rob suggested that for multiset rewriting (over finitely many pattern elements) you could do something like a coin sorter, filtering by size/shape mechanically. it occurred to me this is even closer to the “vector addition systems” style of rewrite rule representation

2025-07-29 15:31:55 UTC

- reply

hmm this book about CAPPs linked in the references seems relevant to my interests
https://storage.googleapis.com/hci-social-storage/media_attachments/files/114/937/240/015/999/278/original/5bd6d4ace657630e.png

2025-07-29 15:28:25 UTC

- reply

is there more to be read about STARAN? like info about its instruction set?

2025-07-29 15:24:14 UTC

- reply

ooh

2025-07-29 15:21:22 UTC

- reply

there’s an orthogonal line of thought here about using rewrites as a bytecode ISA implemented efficiently on top of standard architectures, which i also think is both possible and exciting.
but this question is more for fun, like if you wanted to build a fantasy physical computer where pattern rewrites were your fundamental operation, how would you do it, and how expressive could you make those fundamental operations before wanting to compile them instead

2025-07-29 15:15:28 UTC

spatial rewrite rules, eg:
pacman · dot · empty
↠
empty · empty · pacman
are pretty easy for most sighted humans to run by hand, because we are good at visual pattern matching and replacement.
you can also do general computation this way (think Turing tapes or cellular automata).
digital computers use bits because electricity is better at telling two things apart than many. but what about keys in locks, or loom heddles.. could a machine architecture support pattern rewrites “natively”?

2025-07-22 21:36:49 UTC

- reply

the eduroman empire

2025-07-22 21:36:23 UTC

edurome

2025-07-18 01:54:45 UTC

- reply

it has some obvious things in common with scatting but it seems culturally distant enough not to be directly drawing from that as inspiration. maybe indirectly through rap somehow?

2025-07-18 01:52:03 UTC

is there a word for the thing white male numetal vocalists did a lot in the early 00s like
ooh ah ah ah ah (disturbed)
da bummm da da mm da na ee ma (korn)
was this present in earlier incarnations of metal? I gather there have always been guttural noises/primal screams and whatnot, is there a whole vocabulary of these?
it’s easy to make fun of but clearly also a skill? my mouth cannot make those sounds.

2025-07-18 00:55:01 UTC

- reply

this is absolutely a fair point.

2025-07-17 22:40:16 UTC

- reply

beyond just the education context… there really is a kind of abuser logic to these products. the goal is to isolate you from social support. I think this is probably a really important thing to pay attention to and raise alarms about; I feel like i have not seen enough discussion of it by comparison with other issues (like not working/being wrong)

2025-07-17 22:28:46 UTC

i’ve taught students who are new to programming who try to justify their use of LLM code tools with self deprecation — “i’m bad at this”, “there’s no way i could ever figure it out on my own.” i wish i knew how to get through that the actual value your college tuition pays for is access to live human beings whose job it is to give you the kind of help you’re seeking from the LLM. that those human relationships are what give life meaning & there are so precious few opportunities to create them

2025-07-14 02:25:01 UTC

so where are people looking for reliable covid guidance/reporting these days

2025-07-07 03:10:23 UTC

- reply

i mean just in my neighborhood I know of places to take circus classes, kickboxing, yoga, various martial arts… (actually there’s not a climbing gym and i’m mad about it lol) but a lot of the posts on my neighborhood subreddit are “what gym should i join” and idk if that’s because they actually prefer weightlifting or just assume that’s what one does by default

2025-07-07 02:59:10 UTC

- reply

neither! I’ve tried it, it’s fun, i’d do it more often if I didn’t have other movement options in my life that I prefer. just wondering how and why it became such a ubiquitous default

2025-07-07 02:51:32 UTC

- reply

i have been in physical therapy enough times that i have a pretty good sense for what tends to get under/overutilized in my typical movement patterns and have developed some habits to counterbalance those. but my main form of movement has to be something that i truly enjoy for it to be sustainable and there’s something so transactional about weightlifting that just sucks all the joy out of it. maybe it all comes down to how much i hate counting

2025-07-07 02:42:32 UTC

- reply

ok yeah i buy that one thing weightlifting (and common gym machines) are pretty good for is simulating common functional movements like picking things up, pulling, pushing. it makes sense to have somewhere you can practice a well rounded set of those movements and work on ones you want to improve at

2025-07-06 23:19:07 UTC

- reply

sometimes people will describe climbing and circus arts as “fun alternatives to the gym” but like ?? why is everyone going to the (weightlifting) gym if that’s not the kind of movement they favor?