Stories are proofs of the present.
Proofs  are types  of the terms.
Terms of what?
Terms of an affine variant of the calculus of inductive constraints.

Prufrock is a literary proof assistant.

(Oh, do not ask, "What is it?"
 Let us go and make our visit.)