Post B4pAIPDIrYtlcQW2O8 by chrisamaphone@hci.social
 (DIR) More posts by chrisamaphone@hci.social
 (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!