Port the generic constructions from the paper Completeness of Iris-Based Program Logics. The implementation can be simplified by collapsing the constructive and classical parts into just one big classical construction.
This opens the door to using external solvers for program correctness goals in the middle of a WP proof (eg. Std.do, Aeneas, Loom).
Port the generic constructions from the paper Completeness of Iris-Based Program Logics. The implementation can be simplified by collapsing the constructive and classical parts into just one big classical construction.
This opens the door to using external solvers for program correctness goals in the middle of a WP proof (eg. Std.do, Aeneas, Loom).