1. 11

I used the ml tag because there is no coq tag ):.

  1.  

  2. [Comment removed by author]

    1. 8

      Not only is Coq written in OCaml, but Coq itself is “ML on steroids”:

      • Inductive type families generalize ML’s algebraic data types.
      • (Co)recursive function definitions (Fixpoint, Cofixpoint) are explicitly annotated as in ML (val rec, let rec), and unlike Haskell.
      • Coq’s module system is also ML-like, using signatures to hide module members or make them abstract.
      1. 3

        Yes of course, this is why I’ve finally chosen it (:

      2. 1

        I tag those with programming and math since that seems most accurate.

        1. 3

          It makes sense, especially if the article focus on the “extraction” face of Coq (at least, it justifies better the programming tag).