System Description: CyNTHIA

This paper describes ways of using proofs as a foundation toimprove the situation, in the context of the language ML [4]. The most commonway to write ML programs is via a text editor and compiler (such as the StandardML of New Jersey compiler). But program errors, in particular type errors, aregenerally difficult to track down. For novices, the lack of debugging supportforms a barrier to learning FP concepts [5].