Conversation

rntz
@arntzenius
A lot of PL progress has come by removing stuff that makes reasoning about programs hard. Aliased mutable state, shared-memory concurrency, manual memory management, etc. But... you know what else makes metatheory hard? Variable bindings and higher order functions. 🤔
8
75
rntz
@arntzenius
Replying to
@tom_zwizwa
I'm not sure this is quite what you were asking, but: 1. Variable binding (α-equivalence, substitution, &c) is a classic source of annoyance when doing machine-verified metatheory about PLs. I'm not sure I can briefly explain why.
1
5
rntz
@arntzenius
Replying to
@arntzenius
and
@tom_zwizwa
2. First-class functions complicate lots of implementation & static analysis stuff. They require closures, they can't really be serialized, higher-order state is particularly difficult to reason about, incrementalization of higher-order programs is hard... Does that help?
1
10
Show replies