https://en.wikipedia.org/wiki/Constraint_programming Temporal concurrent constraint programming (TCC) and non-deterministic temporal concurrent constraint programming (MJV) are variants of constraint programming that can deal with time. I am really interested in that. Do you know any material on it? I feel like a lot of boilerplate code today is about wiring/hardcoding the temporal constraints into our codebase. When we want to make sure something works we create the control flow ourselves step by step. Instead, the computer could help us find the “basic” declarative constraints we need and it could generate one (of many) control flow and the correspondent glue code as “implementation”. I am really into this idea, I’d really like to explore this, because I realized I just can’t program without that. It feels incredibly lame. (I am aware of the non-temporal use cases.)

Haskell is pretty much this due to laziness

@Pezo - Zoltan Peto I think I'm facing similar problems at my day job (where we have to control electrical assets), but I can't say I had any epiphany with the research I've done so far. I can share the papers I've discovered, if you're interested.

@Ionuț G. Stan Thanks a lot!

You specify the relationships via code (which creates a code graph rather than a tree). Then, you specify a starting point that takes expression(s) and it will iteratively reduce it (collapsing nodes in the graph along the way) to it's maximal reduction (via typed lambda calculus) The most reduced form shows what constraints are free (usually bounded by types so caught at compile time)

@Don Abrams I am glad you have mentioned Idris, because I wanted to mention it in my response (but deleted to focus on your thoughts) ! 😄 To me Dependent Types seems somehow necessary for that. I think you know much more about that topic, I am only led by my intuition not science. 😄 Is it the time to start learning Idris? I did not find Temporal Logic (especially beyond Linear Temporal Logic) implemented as a lib in Idris. I assume that would be necessary.

On a different note, for constraint solvers (SMT), knowing which constraints are "at fault" is pretty expensive. I'm currently learning enough math to figure out exactly how topoi work so I can more fully understand the stuff Spivak/Fong talk about in the last chapter of 7 sketches (safety proofs in temporal logic). I know basic constraint theory has a bunch of techniques to find locally constrained and locally overconstrained submodels in a model of that's helpful.

cool.. this seems like FRP fused with constraint programming.. putting two crazy paradigms together gets you..?

AFAIK, it means you have a model where you break continuous time into discrete chunks which, when possible, is usually simplifying. Example from what little I know of molecular/chemical modeling: finding the largest time step where you get the correct result is really nice for performance (and hard).