Conversation

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

Replying to

Can you elaborate for the uninitiated?

Replying to

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.

Replying to

and

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?

Tom Schouten

@tom_zwizwa

Replying to

@arntzenius

Thanks for taking the time. For 1. Does this relate to names being an arbitrary way to flatten a graph? Is there a way to represent things more directly (as graphs directly?), or is there a deeper reason? For 2 I can see that you need to somehow carry along context explicitly.

7:35 PM · Apr 4, 2019Twitter Web Client