Design an alternative to the dynamic scope bug

[chameco]

Currently top-level let bindings in SAWScript behave a little strangely. Consider the following:

let COND = true;

let f x y = if COND then x else y;

print (f "foo" "bar");

let COND = false;

print (f "foo" "bar");

This prints "foo" and then "bar" rather than the expected "foo" and then "foo".

While strange, this behavior is sometimes useful (and indeed is used in the s2n and BLST proofs, in order to dry-run sections of the proof during development), so we should provide an alternative. We should consider the remote API in this discussion - fundamentally, I think the usefulness of this "feature" stems from unclear boundaries between the interface to SAW-the-system (imperative, works with proof commands and global state updates) and SAWScript (a collection of DSLs to write specs / proof tactics). Clarifying the boundary between these "languages" would be broadly useful - Coq does something similar here with its "vernacular" command language built atop expression/tactic languages.

[robdockins]

One obvious solution to this is to implement actual ML-style ref cells with more explicit syntax for reading and updating them.