Post #2649824
2026-05-08 14:21 UTC
@mevenlennonbertrand@lipn.info Happy to chat more about this. Roughly the idea is that it’s (1) correct by construction, (2) isolates where all the important syntactic-metatheory results need to be used, (3) completely abstracted from core-syntax and the method used to check equality or invert heads, (4) and the mathematical elaboration definition looks a lot like the Haskell/OCaml code of an elaborator.
The "hard" version that I alluded to also works when the metatheory sucks or isn't yet developed (e.g. like Andromeda etc.).
Replies (1)
-
@mevenlennonbertrand@lipn.info 2026-05-09 10:05
@jonmsterling@mathstodon.xyz I think I have a vague idea of what you have in mind. I guess this is related to the LCF-like approach you mentioned for Pterodactyl a while ago? And I guess the big difference with Andromeda 2 is, as you say, that when the TT does not suck you have access to much more meta-theorems/operations via the interface? I've been thinking about somewhat similar things (although probably not quite) recently, along the lines of "verifying an implementation when you are given only a GAT and its metatheory". This case too should not be extremely hard, but nonetheless interesting. In any case, happy to chat!