Unknown unoptimisable views?

[MattWindsor91]

Currently

{| ? |}

expands to

{| freshname(locals)? |}

where ? means the view can be optimised away.

It might be helpful to have some syntax expanding to

{| freshname(locals) |}

where the view is unknown, but cannot be optimised away. This is basically the user saying 'this is a point where observations can be made about the shared state, so I want to prove axiom soundness here, but I don't care what my view is', and might be useful in cases where we know two commands in sequence are not atomic but we don't care about the intermediate state.

In accordance with what I said in #41 it might be worth coming up with some new syntax for unknown views or advisory views (I hate that name :P) to avoid ambiguity with ?. Maybe something fairly orthogonal like

{| foo(bar) |}   // non-optimisable view
{| ~foo(bar) |}  // optimisable view (should we just call them that, then?)
{| foo? |}       // unknown named non-optimisable view, desugars to {| foo(locals...) |}
{| ~foo? |}      // unknown named optimisable view, desugars to {| ~foo(locals...) |}
{| ? |}          // unknown anonymous non-optimisable view, desugars to {| freshname? |}
{| ~? |}         // unknown anonymous optimisable view, desugars to {| ~freshname? |}

[septract]

What force would this have? Would it actually change what can be proved, or just change the output sent to the solver (and therefore the error message).

[MattWindsor91]

This would just stop the optimiser from doing the more brutal view-removal optimisations on this particular view (the ones that are enabled by adding ? to the end of a view at the moment), and have the semantics of 'I want this view (and implicitly the Hoare triples going into and out of it) proven, I just don't care what it is'.

TBH this is just speculative at the moment, I'd need an example for it first.