Overview

Overview

Like ask, the system will be an interactive environment for programming and proof. The programming language is based on Haskell, but programs are not simply a bunch of equations. Rather, they're an explanation of how the equations were arrived at and of why the program is total.

We have inductive datatypes and program definitions by induction. We have inductive relations and proofs by induction. Old ask allowed only induction on data. New ask should allow relation induction, too.

All ask activities amount to co-writing (with ask) a document which presents a series of (partial) solutions to problems. These all look like

<problem> <strategy> where
  <solution>
  ...
  <solution>

A problem unsolved will begin with a present imperative form of a verb (e.g., define or prove). Once solved, the verb becomes a past participle (defined, proven). Amusingly, completed data type declarations fit this pattern, leading me to consider interactive da problems.

Old ask had no quantifiers (except for implicit universals), so proof problems never gave rise to definition subproblems. Neither had it refinement types, so definition problems never gave rise to proof subproblems. I think that's a pity.