chris martens

go slowly and quietly, and look deep

Public Key

npub15pejcagya70mssj8a5dp6htdkdw93h4wzk952favkktwh40sqs3scmwhd2

NIP-05 Address

chrisamaphone@hci-social.mostr.pub

Profile Code

nprofile1qqs2quevw5zwl8acgfr76xsat4kmxhzcm6hptz69y7ktt9ht6hcqggcpz4mhxue69uhhyetvv9ujuerfw36x7tnsw43q9fllhh

Publishing to

relay.ditto.pub

Author Public Key

npub15pejcagya70mssj8a5dp6htdkdw93h4wzk952favkktwh40sqs3scmwhd2

Show more details

Last Notes

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-29 17:05:24 UTC

despite generally sharing the now-common experience of students never coming to office hours, i have noticed another weird pattern: if i have my door open, students i've never met will just sort of... wander in? and start asking questions? yesterday it was someone in an environmental engineering program who wanted to *measure my window* for a class assignment. today it was someone who wanted to transfer between programs in two different colleges and had literally no idea who to ask.

2026-10-20 23:50:03 UTC

okay why is the number 4 trending* right now
*by which i mean a conspicuous number of posts on my feed from the last hour are about it

2026-10-20 02:18:56 UTC

is there something we can cite as scientific evidence that providing lunch at a gathering is a good idea? surely *someone* has done this research. easy path to impact and citations

2026-10-11 18:21:50 UTC

someone sent me a nice personal (i thought) note about a project i worked on over a decade ago. after mulling over it in the back of my head for 3 days while attending to more urgent matters, i finally wrote a response. the reply comes 7 minutes later and ends with "(full transparency: i'm [name]'s AI assistant, helping him with emails)"
this shit is going to break me yall.

2026-10-04 03:12:27 UTC

i have been sick all week, so on account of canceled meetings and social activities i have actually finished things (two small agda projects, a bookbinding prototype, a confusing novel, fridge leftovers)

2026-09-25 19:15:51 UTC

what's your favorite way to represent (discrete) numeric ranges with dependent types? (e.g. what's the type of "numbers between 6 and 9")

2026-08-28 12:49:18 UTC

badge customization
https://storage.googleapis.com/hci-social-storage/media_attachments/files/117/173/211/372/620/903/original/03169c8218c41523.jpeg

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-24 16:27:30 UTC

the body has no normal form
(out of context PL quotes)

2026-07-18 20:29:25 UTC

i know i'm like 14 years late on this but: the FTL soundtrack is so good. game's not bad either

2026-07-13 19:26:11 UTC

i've been fascinated by and closely following this PennDOT project to replace a major highway bridge in pittsburgh:
https://www.pa.gov/agencies/penndot/projects-near-you/district-11-projects/commercial-street-bridge-replacement
i'll adopt a friend's affectionate nickname "boom-and-scooch": they've constructed the new bridge *next* to the old one; they are in the process of demolishing the old one and then they'll *pick up and move* the new one into place (a "lateral slide")

2026-07-03 02:09:48 UTC

- reply

@nprofile…vsjg 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-22 20:33:05 UTC

- reply

@nprofile…0f5x lol. it depends on the type theory... some of 'em know my weaknesses

2026-06-22 19:11:17 UTC

showing someone a type theory and asking if they've seen it before like a detective passing around a photo of a perp

2026-06-20 17:03:36 UTC

- reply

@nprofile…awd8 i mean software for doing computer-assisted theorem proving, such as Rocq, Lean, and Agda

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-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-28 11:58:42 UTC

- reply

@nprofile…pfuj i have heard a theory that the Drink More Water dogma is somewhat flawed in that a) we also need electrolytes and drinking lots of water flushes those out; b) we do get water from food and if you're eating foods with high water content you probably don't need to follow the "8 glasses a day" rule. my just-so-story guess is we probably evolved with foods that were higher water content & didn't need the instinct to drink plain water so much

2026-04-25 17:54:10 UTC

i assume i'm not the only one who, upon getting a software update with a noticeably worse default experience, goes in to change the settings and then notices and turns off a bunch of other privacy-invasive or engagement-motivated features. i wonder if there's a term of art for this behavior

2026-04-17 18:57:03 UTC

trying this on: i want to characterize my interests that pertain to games, simulations, procedural generation, programs that draw pictures, and computational models of narrative as "systematic media" or "systematic art."
the point is the rules that define these things are carefully constructed and refined, meant to be transparent and legible to humans. this has very little in common with what "generative art/design" now means to most people, unfortunately.

2026-03-30 16:32:18 UTC

- reply

@nprofile…3q9y settling in at all yet?

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-02-18 14:44:12 UTC

- reply

more like capitalist letters amirite

2026-02-11 14:16:49 UTC

- reply

@nprofile…xuzd oh wait what are the two halves? this is a world i don't engage with much

2026-02-11 14:07:11 UTC

- reply

@nprofile…xuzd the one that always surprises me is how close gentzen's original formulation of natural deduction and sequent calculus are to what we use today. but yeah, in general, my findings definitely agree with yours

2026-02-11 14:00:22 UTC

good stewards of other people's ideas impress me more than the first people to write them down

2026-02-06 01:13:48 UTC

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

2026-02-03 19:21:29 UTC

- reply

@nprofile…xuzd cool cool. i wasn’t quite sure because my first mental association via incremental-as-in-computation was about object level programs (rather than incrementalising the meta level program that typechecks your language)

2026-02-03 19:05:13 UTC

- reply

@nprofile…xuzd what do you mean by “incrementalise” here? like loading in declarations one at a time?

2026-01-26 12:07:31 UTC

just saw someone use the word jants to refer to the long version of jorts

2026-01-13 02:10:00 UTC

today i learned lean has distinct “monad” and “lawful monad” type classes. i’m aghast they botched the opportunity to have named the first one “chaotic monad” instead

2026-01-12 22:41:26 UTC

the propaganda: give corps all my data and they’ll ~personalize my experience~
the reality: a text message beginning “hi tom”, to a tom who is in my contacts, autocorrects to “hi Tim,”

2025-12-30 01:19:12 UTC

- reply

5. this is more of a comment than a question but i think this is an incorrect use of the concept of tasting notes. however I may not understand the concept well myself
6. did they just ask someone to drink the tea and say what they thought it tasted like? i can respect that actually. i think that’s consistent with what i remember from a coffee cupping or two many years ago

2025-12-30 01:06:12 UTC

i have an herbal tisane that lists “orange peel, pomegranate, and lemon” as its “tasting notes” while the literal ingredients are hibiscus, orange peel, lemongrass, elderberries, apple, rooibos, & stevia. several questions.
1. what gives orange peel the esteemed status of both a tasting note and an ingredient?
2. are ingredients allowed to be tasting botes?
3. if so, why aren’t all of them?
4. if you made a tisane out of orange peel, pomegranate, and lemon, what would its tasting notes be?

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-27 02:33:00 UTC

hatters gonna hat

2025-12-24 15:32:14 UTC

- reply

@nprofile…rrqe nice! thanks for sharing what you're reading. i really enjoy slice of life posts like this.

2025-12-18 14:24:43 UTC

- reply

@nprofile…rrqe hmm, allowing undo/backtracking over choices does seem like a user friendly thing to do, but i honestly wasn't imagining "good" usability as a goal of a first MVP

2025-12-18 14:12:06 UTC

for ages I’ve had this dumb idea to systematically generate UI widgets for constructing strictly positive types. labeled sums turn into dropdown menus for each constructor, records are panels of widgets for each field, finite integer ranges become sliders, strings become text fields. self reference is fine because you only expand the top level of the pattern. does anyone want to help me make this so i can get it out of my head

2025-12-17 23:36:39 UTC

- reply

at one point publishers & professional societies played a role that I thought was important, of helping the public tell apart sound scholarship and science from misinformation and opinion. it’s clear now that neither they nor the public actually care about this distinction. so the main role they play now is an “internal” one, a tool for our community to help each other access and judge and reuse our work. is it working for that? can we do better?

2025-12-17 23:24:48 UTC

thinking about how we all* collectively hold each other hostage to publishing with ACM as part of what it means to have a good research reputation
(well, academics in the US anyway, but also I’ve seen the venues mentioned in European job ads)

2025-12-11 00:18:17 UTC

caprese is the plural of capri sun

2025-12-05 16:59:55 UTC

there’s this old recording of bertrand russell telling a story of having to receive guests as a child when the adults of the house were away and some older gentleman asking him, “‘it’s a very fine port they’ve given me; but why have they given it me in a claret glass?’ and *I* didn’t know the answer!”
I need this to become a meme because i constantly want to snowclone “it’s a very fine _ but why have they _”

2025-12-02 21:40:12 UTC

chess, a “dark souls” of turn-based strategy games,

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-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-11 15:47:17 UTC

I know I’ve heard about at least one human subjects experiment and/or interviews of proof assistant users on here — can anyone remind me who was doing that and if the paper(s) are published?

2025-11-10 01:10:26 UTC

folks who mechanize theories and proofs*: i am curious about your documentation practices. have any of you developed a consistent approach to writing comments, doc pages (generated or manual), or linking code to prose explanations (e.g. in papers)? have you written about it somewhere?
*i’m most interested in “end users” of proof assistants rather than implementors, but i’d also consider libraries to be in scope.

2025-11-09 02:57:19 UTC

I have passed this sign dozens of times and it only just occurred to me to question this choice and placement of punctuation
https://storage.googleapis.com/hci-social-storage/media_attachments/files/115/517/487/406/854/533/original/8bce6d07282011b2.jpeg

2025-11-05 15:19:18 UTC

- reply

@nprofile…ral2 wait, as in, they’re saying “assume not-A is not the case” and then proving not-A directly (by assuming A and deriving contradiction) to contradict it?? or .. somehow using the assumption of “not-A false” in two different scopes?

2025-11-04 22:53:45 UTC

it’s always “early career” this, “under 40” that, where’s the “wow this person is suddenly trying to pivot to a new career in their 50s and seems like they could make a proper go of it if we just sprinkled them with a bit of fun money for a year” award

2025-11-01 18:18:07 UTC

- reply

@nprofile…zjv9 (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-28 22:16:49 UTC

- reply

i could have sworn i once saw something from @nprofile…w8t5 like this working up from finite types (1, 0, product, sum) to w-types with a general recursor, but i cannot seem to find it.

2025-10-28 22:12:17 UTC

hey sooo anyone have good course notes or similar on inductive types (*not* arbitrary recursive types)? your own or someone else's?
i personally don't mind chapters 14-15 of PFPL but they're a little more cryptic than i'd like (perhaps because it dances around the category theory).

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-20 23:14:25 UTC

- reply

@nprofile…rrqe on a more serious note, I really enjoyed your talk, and in particular i admire the care you took to explain related work, amplifying other people’s ideas that have been overlooked. it’s clear you really took the charge of understanding many different proof systems seriously, and as a result you developed the right vantage point to say true and fair things about all of them

2025-10-20 20:56:49 UTC

@nprofile…rrqe I was made aware of the alarming fact today that pterodactyls are not direct ancestors of birds. does this have implications for the future of proof assistants?

2025-10-15 22:19:12 UTC

- reply

@nprofile…w8t5 incidentally i was in an interesting discussion recently wherein someone didn’t know what i meant by “informal proof” and a group of us collectively struggled to define it. I wonder if you have a good way of articulating the separation between formal and informal you have in mind (and whether it matches my own ideas)

2025-10-15 16:01:45 UTC

a lesson i take from certain authors in my field is that if you give a silly name to an important enough idea, you get to hear important looking people saying silly things. and perhaps that can be motivation enough for some of us

2025-10-07 14:56:00 UTC

some of my favorite people work at Token Transit, a company that builds flexible fare payment systems for public transit agencies. they’re currently hiring a senior software engineer for their small, fully remote team (6 engineers, 12 total employees):
https://jobs.gem.com/token-transit/am9icG9zdDqr6LOSS-gA5BpaFiKlKfwt
🔁 ✅ #getFediHired

2025-09-30 04:20:05 UTC

#tilingTuesday
a walkway in Tokyo
https://storage.googleapis.com/hci-social-storage/media_attachments/files/115/291/322/740/104/502/original/f1f24eec54b2f0a8.jpeg

2025-08-27 21:13:30 UTC

whats large about large eliminations?

2025-06-18 12:52:18 UTC

- reply

@nprofile…6kk0 scary! Are you ok?

2025-06-16 08:57:21 UTC

- reply

@nprofile…jqvx @nprofile…d23x @nprofile…w9qq doctors hate her! try these totally normal tricks to stymie a medical system built on statistical fallacies

2025-06-12 09:19:29 UTC

slides for my TYPES 2025 talk, "a guided tour of polarity and focusing", are available here:
https://chrisamaphone.hyperkind.org/types-2025.html
it was recorded, but the recording may not be up for awhile. if you have questions about anything on the slides in the meantime, let me know!

2025-06-10 12:53:15 UTC

nice TYPES talk by @nprofile…n8ju on connections between type theoretic and philosophical perspectives on logic! https://consequently.org/presentation/2025/type-theory-and-phil-logic-types/

2025-06-09 10:45:31 UTC

today's PL history hunt: where *does* the term hereditary substitution first appear?
the *idea* is i think correctly attributed to kevin watkins and described in a 2002 unpublished CLF tech report (https://www.cs.cmu.edu/~fp/papers/CMU-CS-02-101.pdf).
but that TR calls it "instantiation." part 2 of the tech report (https://www.cs.cmu.edu/~fp/papers/CMU-CS-02-102.pdf) renames it "canonical substitution" (without acknowledging that part 1 uses a different term!). the word "hereditary" appears nowhere in either.

2025-06-08 13:31:54 UTC

writing this TYPES talk is basically taking me down the road i would have gone down for my dissertation if only, well https://hci.social/@chrisamaphone/112099893061121398
that is making it surprisingly emotional work. and i don’t have time to write a dissertation by thursday. but i am glad to be doing at least some small piece of this

2025-06-06 22:49:45 UTC

- reply

@nprofile…r9rs @nprofile…mmpy arguably an app and/or website is solving a social problem *within this very interaction*

2025-06-06 21:08:40 UTC

one of my “is it the future yet” things for software is i want default palette-swapping options in every visual design & illustration tool. there is no reason i should have to go change a color manually when i use it consistently in many places

2025-05-26 18:44:59 UTC

datalog : graph reachability
::
dependent types : length-indexed lists

2025-05-26 12:13:05 UTC

💭 oplss but for professors

2025-05-23 23:37:42 UTC

choosing your gender and sexuality based on what pride flag colors you like best

2025-05-20 19:45:26 UTC

wait there are people who think inability to make eye contact in virtual meetings is a downside and not a benefit?

2025-05-16 15:42:01 UTC

to be fair, programming would be a *terrible* way to get out of a paper bag

2025-05-16 02:38:12 UTC

you can't spell mcdonalds without monads

2025-05-14 00:14:38 UTC

my one and only answer to how to buy clothing (and other stuff) of decent quality is to get it second hand and know what to look for, but that doesn’t always cut it if you need something specific. non-rhetorical question: where do you turn/what process do you follow to find things with specific criteria that can only be evaluated in person (like fit and feel)?

2025-05-12 00:56:43 UTC

wild how most of tidying up is just picking up items and setting them down in different places. why should that change anything

2025-05-11 02:56:25 UTC

awhile ago someone posted a screenshot of some birding subreddit where the exchange was like
OP: saw bird, not sure what kind
Comment: did you get a picture?
OP: nope flew away
Comment: happens
but i keep failing to re-find it. anyone else?

2025-05-08 01:28:04 UTC

this came through my inbox - Processing (https://processing.org/, the originally-java-based drawing/animation language) is hiring a Project Lead "to guide the maintenance and growth of the Processing software." full remote, fixed $95k salary (this seems low by corporate standards but they're a nonprofit). could be a fit for someone in my network-proximity... https://processingfoundation.org/employment/processing-project-lead

2025-05-03 23:43:19 UTC

- reply

@nprofile…nrqy i have not seen The Room but that is SO CUTE

2025-05-01 14:59:55 UTC

i can think of a few projects that fit the following bill: an implementation of a dependently-typed language/proof checker that
- has a formally well-defined and documented type theory
- is "small" and not intended to "scale", i.e. is intentionally kept minimal and amenable to study as a formal system
- can run on a computer today
reply with your favorites?

2025-04-30 23:13:45 UTC

one could put pictures of their cats on a telephone pole even if the cats are not missing

2025-04-24 13:07:33 UTC

what’s a book that you hated but read all the way through?

2025-04-21 22:26:58 UTC

so, hey, if any of my US academic friends are well connected to industry partners or private foundations or whatever who still want to fund research that values the participation of underrepresented groups and/or being able to distinguish truth from fiction, i’d love an introduction? seriously, if you know anyone who might fund my group’s work (types, logic, proof assistants, etc.) this is something that would be materially helpful to me and my students.

2025-04-21 18:24:28 UTC

holy shit this is bleak: https://www.nsf.gov/updates-on-priorities
the part about "misinformation/disinformation" was new to me. the verbal gymnastics performed in the final sentence of that section gives me something to aspire to as a student of circus arts

2025-04-13 18:43:20 UTC

i recently learned* this nice multi-signature booklet/zine binding technique that doesn’t require adhesive *or* sewing! you cut slits in the middle of each signature, make an accordion whose mountain folds fit through the slits, then secure each mountain by sliding a strip of paper through it on the inside of the signature
(*from the “Wanderlust” online art class: https://www.everything-art.com/)
#bookbinding #papercraft
https://storage.googleapis.com/hci-social-storage/media_attachments/files/114/332/102/365/220/254/original/285021a438eeae1c.jpeg
https://storage.googleapis.com/hci-social-storage/media_attachments/files/114/332/102/400/263/534/original/1962405d8a06f525.jpeg

2025-04-09 21:33:29 UTC

- reply

I don’t normally swear in class, but this isn’t normal.

2025-04-09 21:29:12 UTC

a student interrupted the start of my lecture today to say goodbye bc their visa was revoked and they needed to leave the country immediately. great job we’ve done everyone

2025-04-05 03:06:39 UTC

- reply

@nprofile…jkwt @nprofile…veyj @nprofile…vddj ah yeah this was definitely from an undergrad culture perspective (i was a cmu undergrad when i met folks at MIT). grad student culture is often very different

2025-04-05 02:49:41 UTC

- reply

@nprofile…vddj @nprofile…veyj @nprofile…jkwt this confuses me bc my first interaction with MIT students involved tunnel hacking and mystery hunt

2025-04-03 21:35:40 UTC

who else constantly gets distracted looking for 2FA devices/codes and comes back to timed out logins

2025-04-01 11:48:53 UTC

belatedly, if you’re confused or skeptical about “trans day of visibility”, you’re in good company; @nprofile…jqvx has been writing good stuff about it for years, including this one: https://bsky.app/profile/dryad.technology/post/3llphepns2k2h

2025-03-30 01:38:00 UTC

i’m say chromosomes are to gender essentialists as skull shapes are to phrenologists, except you can’t feel your chromosomes with a set of calipers

2025-03-20 13:17:32 UTC

- reply

@nprofile…6m2n are you familiar with the term “notional machines” the way CS education researchers (and CS educators I think) use it? seems applicable to what you’re talking about here wrt mental models and to what extent it matters if pedagogical explanations are actually conformant to implementations

2025-03-13 16:09:01 UTC

- reply

@nprofile…ekkm @nprofile…r9rs idk i do think of my brain as being “built for puzzles” in a way but I have this experience with puzzle games all the time - i rarely 100% them, and sometimes i look up hints and solutions - but for me this doesn’t detract from my appreciation for them

2025-02-10 18:12:09 UTC

- reply

@nprofile…6kk0 what’s your workflow for running code? Compiling or normalizing stuff in the editor or something? is there a good repl/ghci approximation (proof interactive mode I would guess might work)?