Languages and Systems for Interactive Proofs