I’ve said it before, I’ll say it again: we need a protocol for proof assistants!!!
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
PGIP is interesting, but my take is that we should be more radical. Instead of using a client/server model, we should think of the proof assistant as a database that supports some sort of query language
2
3
There are a couple of reasons for doing this! It makes editors less privileged than other tools that may want to inspect/interact with the proof assistant. It also means that it's easier to write complex refactoring tools without extreme levels of pain
1
1
This does make implementation somewhat more tricky, but I think we can design libraries that can do a lot of the heavy lifting for you
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Exactly. However, rust-analyzer still has to go through LSP. I'm saying we chuck that step out entirely and expose the query language /as the protocol/
2
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
I will always defer to the IDE masters here lmao
1
1
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
I think he still contends that the Dart editor protocol is a better design, but they use the LSP out of necessity. Been trying to get him interested in typed holes but yeah, I'm not very good at selling this stuff other than ‘try Adga/Idris’ or ‘it's cool!’.
I think he might have been soured by his experience with Jetbrains MPS and so it's kind of hard to say ‘no, this stuff is not like that’.
2
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
Show replies