Conor Titania Mc Bride2d ago

So here's a thing.

The proof assistants we need for professionals advancing the frontiers of our understanding are not the proof assistants we need in the education of our youngsters.

The feedback they need and can have is wildly different.

I want to contribute to both projects, but perhaps I can help by observing that they're not the same project.

Show threadDima Pasechnik 🇺🇦 🇳🇱

@pigworker how about proof assistants for proofs that last a while?

I mean, even C code bitrots (and C++ bitrots horrendously) - the much more complicated languages rot even faster. Maths written up in English before 1900 is very hard if not just impossible to read. Many 60-years old papers which are part of the Classification of the Finite Simple Groups (CFSG) are very hard to penetrate (the topic went out of fashion very fast, this didn't help). Etc.

Mar 28 at 5:38amWeb
Show threadConor Titania Mc Bride1d ago
@dimpase This is a hard problem, but it is strongly worth considering. Programming languages ted to be designed from a purely synchronic perspective, as if they have no diachronic life worth thinking about. And then that diachronic life bites you. That function you wish was in the library gets added to the library and now your code has a duplicate definition...
Show threadDima Pasechnik 🇺🇦 🇳🇱1d ago

@pigworker Any PL people want to join, in some capacity, forces, in a grant pre-application for the next round renaissancephilanthropy?

I do have a couple of publications in this direction, although they are quite simple-minded.
@TaliaRinger

Show threadConor Titania Mc Bride1d ago
@dimpase I have a particular thing I'm thinking of pitching in that direction, based on my perturbation testing stuff. I'm open to other possibilities. @TaliaRinger