Post #4119653
2026-05-29 13:08 UTC
@rntz@recurse.social I think it basically amounts to the fact that Lean is using the language server protocol to vend semantic highlights directly from the compiler. This is actually a better approach than using something like tree-sitter (or, god forbid, regexp), even for languages without metaprogramming, for the simple reason that you don't have to maintain two grammars. But it does mean that you have to trust the code.
Replies (1)
-
@rntz@recurse.social 2026-06-01 07:57
@jonmsterling@mathstodon.xyz I think “maintain two grammars” is better for the ecosystem than the tacit expectation that we trust the codebase as soon as we want to check a proof. This is getting into “wish list” rather than “reasonable expectation” territory, but given the rise of supply chain attacks I’d like to see more sandboxing / safety guarantees from new languages, not less, especially when it comes to things like theorem provers that might in principle be used to verify untrusted code.