jacobjwalters

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 structures. My experience with getting Claude (even fable) to do step indexed logical relations/SL proofs autonomously is that it struggles hard even on toy examples, particularly around the index shuffling. Do you have a setup in mind that can scale to larger programs?

Fun project in any case! I look forward to seeing how it develops :)

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 statically? How can I make sure these do not overlap? And since this is a shallow embedding into lean, what’s the approach for verifying properties of non-terminating programs?

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, with the main characters largely just along for the ride. It takes the science parts super seriously too: ships have to worry about acceleration and debris fields during battle, communications have to account for the speed of light, that sort of thing. There's only the occasional injection of new technologies to push things forward about once per book/season.