Type-Safe Dynamic Placement with First-Class Placed Values
Explore a 16-minute conference talk from OOPSLA2 2023 that introduces Dyno, a programming language enabling static reasoning about dynamic placement in distributed systems. Discover how Dyno's type system with first-class placed values and novel interpretation of dynamic placement as unions of placement types ensures type safety and placement correctness. Learn about the formalization of type soundness, placement correctness, and architecture conformance. Examine case studies and benchmarks demonstrating Dyno's effectiveness in enabling static reasoning for programs with dynamic placement at minimal performance cost. Gain insights from the reimplementation of an Android app with 7K LOC in Dyno, uncovering a bug in the existing implementation and revealing common dynamic placement patterns in over 100 open-source apps.