In this course, I will survey some recent progress on this problem, based on the striking observation that it is possible to give types to reactive programs using the formulas of temporal logic.
From the perspective of proof theory, this leads to a Curry-Howard proof term assignment for constructive temporal logic. These proofs support a denotational semantics which is a natural generalisation of the model-theoretic semantics of LTL. Furthermore, from the view of programming, we get a programming language which is simple, highly- expressive, and easy to implement.