Posts by chrisamaphone@hci.social
 (DIR) Post #AkL2lvgTLIFxzmggfQ by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       not all tasks require the entirety of your ass
       
 (DIR) Post #AtQiR3xDaqQcHNrm8e by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       i *do* have better things to do than shitpost at the moment, but look, this is the situation
       
 (DIR) Post #Av7sW3Z64SSwxFEVBw by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       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! update: recording available now! https://youtu.be/EbcEX2SyObs?si=dVx6ptl7BfbdookU
       
 (DIR) Post #B4WG4ADYjDS2mFzNbc by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       current progress on becoming @justinefrank
       
 (DIR) Post #B4ku8d0AMuPHaSqa0G by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       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
       
 (DIR) Post #B4pAIOW3SMItSIHUye by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       new from me, @etosch , @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.pdfpresented at PLATEAU a few weeks ago. slides: https://khoury.northeastern.edu/~cmartens/talks/plateau-itfp-talk-slides.pdf
       
 (DIR) Post #B4pAIOkwZ0DICTFOBU by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       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
       
 (DIR) Post #B4pAIP0BeKPGxkNYwa by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       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
       
 (DIR) Post #B4pAIPDIrYtlcQW2O8 by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       people shouted out in the talk include @ionchy (for their lovely reproduction of Reynolds' "types, abstraction, and parametric polymorphism"), @MartinEscardo for his posts about Agda as communication tool, and @david for letting me ask annoying questions about his Lean projects :)
       
 (DIR) Post #B4pAIPTbsvwUR093o0 by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       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!
       
 (DIR) Post #B4pAIPfJBRIf1HcP2W by chrisamaphone@hci.social
       0 likes, 1 repeats
       
       re: https://hci.social/@chrisamaphone/116325060049701188taking 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.RT: https://hci.social/users/chrisamaphone/statuses/116325060049701188
       
 (DIR) Post #B4pB5Z2N7xDsHAqLWC by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       @neauoire thanks! i'm interested in hearing what you think if you have a chance to read further on
       
 (DIR) Post #B4pCT3ymLr6sr6vpNg by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       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 @simrob for planting this lexical seed in my head)
       
 (DIR) Post #B5lWVOsUtAxeVD3qaW by chrisamaphone@hci.social
       1 likes, 1 repeats
       
       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.
       
 (DIR) Post #B6DxGQ2iPiJGxYncZs by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       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?
       
 (DIR) Post #B6DxGSzdRcd26sNhh2 by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       a related thought i've been having is that i find it hard to get excited about "maker spaces" where the main creative processes supported are sending data to a machine and supervising it while avoiding hazardous dust and fumes
       
 (DIR) Post #B6kroCCkf21xk3e1dQ by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       @futurebird 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
       
 (DIR) Post #B6lonCyAE7Kb7TcQ6a by chrisamaphone@hci.social
       0 likes, 0 repeats
       
       @shapr this has "jesus is my copilot" energy
       
 (DIR) Post #B7ecpt6wJ7THKM4sm8 by chrisamaphone@hci.social
       1 likes, 0 repeats
       
       my decision to stay fluent in a programming language with a stable legacy implementation of a 1997 formal definition feels pretty good these days
       
 (DIR) Post #B7ofmOCl0BZQ32QCSO by chrisamaphone@hci.social
       1 likes, 0 repeats
       
       sneak preview of latest collab with @simrob