Non-Eternalist Logic #3

Dynamic Hoare Logic

1. Turns out there are some other precursors to this seemingly outlandish notion. For instance, Propositional Dynamic Logic which weds traditional Propositional Calculus, Modal Logic, Programming Languages, and Program Execution.
2. Like Temporal Logic, static (fixed) Expressions describe dynamic or changing States (but do not themselves change).
3. Instead, variant States are modeled using Possible World Semantics (e.g. - as Kripke Frames or Modalities) so that all permissible States are presented as branching diagrams (or as Accessibility Relations, to be more precise).
4. Can we think of Hoare Expressions in a way so that {Q} changes based on {P} (Given {P}S{Q})? Is this a trivial or special case of a known kind of Hoare Expression?
5. How would this generalize and what properties might it exhibit?

A simple Hoare-like scenario:

const P = 0

let q = 0

if (P === 0) q++

const Q = q < 2

Suppose Q is Curried or transformed into Higher-Order Function?

let P = 0
let q = 0
let Q = false

// S
const R = Math.random()
const qQ = f => (...args) => f(args)
const A = q => q === 0
const B = q => q > 1
const C = q => q < 0

if (R < .5) P++
if (P === 1) Q = qQ(B)(q)
if (P === 0) {
 q+=2
 Q = qQ(C)(q)
}

console.log(P)
console.log(q)
console.log(Q)

Condition P is subject to change and Q accepts a variant Higher-Order Function that changes the evaluation of q (despite the resolved value of q being true under B):

# Where P is 1
1
0
false

# Where P is 0
0
2
false

In the above scenario P, Q, and q are bounded by a finite range of possibilities (and so give rise to the kinds of Modal Semantics alluded to above) despite the evaluation Q to be modified.

It looks like there's some fairly nascent research on these topics (less than 20 years old, Higher Order Functions, etc.):

1. https://cambium.inria.fr/~fpottier/publis/regis-gianas-pottier-hoarefp.pdf
2. https://arxiv.org/pdf/0806.2448v2

I have some questions (and regrettably I haven't looked into the literature too much) and my curiosity has gotten the better of me here:

1. What about scenarios where S doesn't halt or the mutability of Q continues indefinitely?
2. What happens when Q's evaluation calls P?
3. What happens if we were to say write random Strings and eval (them, the randomly generated but syntactically-valid) somewhere in P, S, or Q - do we have many Modal universes semantics-wise? (That's certainly allowed in JavaScript.)
4. How does a Hoare Expression fit into the contexts of Quantum Computing (specifically, Quantum Entanglement, Unitary Evolution, and Superposition of Qubits)? Q presumably would require some Measurement or resultant Quantum State. (Quantum Measurement/Observation seems to align with the idea of Evaluating some condition or State.)
5. What about a scenario where the evaluation of S (its output) changes that output?
6. How do the above violate the Hoare Composition Rules?