jacobjwalters

3 ms·

1. 1.▲
   by jacobjwalters 4mo ago

   Is the plan to build a new separation logic framework, or use e.g. iris-lean or splean as a base? And even if fuel isn’t exposed in the program logic, I’d imagine you’d still want step indexing to allow reasoning around cyclic heap structur
2. 2.▲
   by jacobjwalters 4mo ago

   What is the program logic used here? The num_integer verification example seems to be hardcoding addresses in the spec; what if I want to reason about larger programs that dynamically allocate, where the addresses may not be known staticall
3. 3.▲
   by jacobjwalters 10mo ago

   The Expanse (both a recently completed book series and a cancelled yet mostly complete TV adaptation) is pretty good at this; it sets up a world with complex political dynamics, and lets things mostly evolve as a result of those dynamics, w