Conor Titania Mc Bride

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.

Mar 27 at 10:01pmWeb
Show threadConor Titania Mc Bride1d ago
In particular, the professionals tend to work solo, or in tight teams, solving problems they hope are fresh. In education-land, the weans are getting to grips with old chestnuts, so there are more interesting ways to address failed proof attempts, in a cohort.
Show threadPhilippa Cowderoy1d ago
@pigworker Amongst other things, that sounds like something you could legitimately throw machine learning techniques at over time! Though any chatbot-like UI should have clear indications of being "ELIZA with domain expertise and a log"...
Show threadSam1d ago
@pigworker it's almost like we don't give beginner programmers huge stacks of monad transformers or C++ templates on day one
Show threadterru1d ago
@pigworker attempted to teach students how Isabelle works recently. Ran into trouble: “by simp” can do (almost) all the proofs in introductory things. how convenient! but nothing is learnt … 🙈
Show threadConor Titania Mc Bride1d ago
@stuebinm I can see how that's frustrating. My gadgets are both too stupid and too clever. It's worth thinking about how to adapt.
Show threadDima Pasechnik 🇺🇦 🇳🇱1d ago

@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.

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
Show threadJan de Muijnck-Hughes1d ago

@pigworker no shit! (But a positive shit)

I’ve long thought about the tools we give learners when thinking about how we teach programming.

We can compare programming languages and their standard libraries with tools for carpentry.

I had many toys of various sharpness, as I progressed, when being taught basic wood working. First plastic tools, then real and kid friendly saws and hammers, then a proper toolkit.

We do not do this with programming (or theorem proving). Learners need training wheels (e.g. a learner focused prelude) before being sent to the standard prelude!

Show threadJeremy Gibbons18h ago
@jfdm @pigworker "We" don't do this, but the Racket folk have done it for decades. It's a shame we don't have language levels in Haskell. It's even more of a shame that the language is actively heading in the opposite direction.
Show threadJeremy Gibbons16h ago
@jfdm Of course, there was Helium from Utrecht that went part way there.
Show threadGuillaume Andrieu14h ago
@jfdm @pigworker I definitely like this analogy with woodworking because it is meaningful at several levels. You do as fine woodwork as your tools are sharp, and so mastering joinery is pointless unless you know how to sharpen the tools efficiently. It is imperative to learn both. You must know not to attempt to sharpen a very dull blade with a very fine stone, this would take forever. You always start with a coarser grit before gradually moving to finer ones. Similarly when learning new concepts, getting a rough idea before gradually refining is more efficient than attempting to learn from academic literature. What I often miss is the fine/middle grit. Rough ideas can be found (but it is often hard to judge their quality or which way they point at when you start), finest/honing ideas are plenty on the arXiv, but the intermediate is nowhere to be found for people like me who left the universities decades ago now, so I feel a bit stuck.