We propose a logic of interactive proofs as the first and main step towards
an intuitionistic foundation for interactive computation to be obtained via an
interactive analog of the G\"odel-Kolmogorov-Art\"emov definition of
intuitionistic logic as embedded into a classical modal logic of proofs, and of
the Curry-Howard isomorphism between intuitionistic proofs and typed programs.
Our interactive proofs effectuate a persistent epistemic impact in their
intended communities of peer reviewers that consists in the induction of the
(propositional) knowledge of their proof goal by means of the (i