Post #4398822

2026-06-01 07:57 UTC

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

Replies (1)

@jonmsterling@mathstodon.xyz 2026-06-01 08:03

@rntz@recurse.social I note that in your reply you say "we trust the codebase as soon as we want to check a proof" rather than "as soon as we want to look at a syntax highlighted proof". We could debate on the latter, and maybe maintaining two grammars is reasonable in some cases, but for the former, there never has been any alternative to running the code for checking proofs — going all the way back to LCF. You want to check the proof, you have to run the code. I think existing sandboxing is clearly the solution to this problem, but it isn't something that should be solved at the language level. Sandboxing is already a solved problem via containers, etc. If you are concerned about pwning yourself by running someone's Lean code, you should run it in a container.

Open ##4398824