Many of the ideas you discuss here were formalized in the 70s by Amir Pnueli and others into the LTL and CTL temporal logics -- ideas that still form the core of much of software verification today -- and those heavily influenced both Lamport's temporal logic TLA and specification language TLA+, and the synchronous language Esterel, by Gérard Berry[1] (Wikipedia says that the synchronous language Lustre was influenced by Lucid) -- "time doesn't exist between stable states". Both TLA+ and Esterel have achieved a certain degree of success in the industry (to this day), although mostly in safety-critical realtime software and hardware design; the ideas are just starting to flow to "everyday" software. While they have a very explicit, clear notion of time modality and are "pure", they are not functional.

I think that as many ideas are crystallized, it is no longer helpful to characterize every pure and/or temporal-logic approach as functional; indeed, the two notions may often be at odds. (Pure) functional programming, at least as (sort-of) defined today. FP is not directly about modeling time and certainly does not impose synchronicity (a clock), but is more about the idea of denotational semantics, where computations are imagined as functions, and function application imposes an equivalence relation (the function application is said to be equal to its result in this relation). This is very different from the philosophy of synchronous languages.

[1]: The modern language Céu is based on Esterel: http://ceu-lang.org/