We build computer systems around abstractions. The right abstractions are timeless and versatile, meaning they apply in many different settings. Such abstractions make developers’ lives easier, and allow system developers and researchers to optimize performance “below the hood”, by changing systems without breaking the abstractions. In this post, I will argue that the abstraction of … Read more The Remarkable Utility of Dataflow Computing
The POPLmark Challenge helped stir lasting excitement about mechanized proofs within the PL community. Despite the advances and successes, there is a lot more to do. This post reflect on the state of affairs of mechanized proof in PL, organized around the topics and discussions that arose in the POPLmark 15 Year Retrospective Panel.