1. 7

  2. 3

    This is a good demonstration for the power of abstract types. A user-provided string is marked as dirty and it can become a clean usable ordinary string value only by scanning it for problems such that this never can be missed.

        module DirtyString : sig       (* interface *)
          type dirty_string               (* abstract *)
          val dirty       : string -> dirty_string
          val escape      : dirty_string -> string
          val read_int    : dirty_string -> int option
          val read_ncname : dirty_string -> (string * dirty_string) option
        end = struct                   (* implementation *)
          type dirty_string = string
          let dirty = %identity
          let read_int = int_of_string_opt
    1. 1

      We have identified (more than a decade ago, in fact) a disciplined programming style that uses existing type systems in practical, mature languages (such as OCaml, Scala, Haskell, etc., and to an extent, Java and C++) to statically assure a wide range of safety properties:

      • never dereferencing a null pointer or taking the head of an empty list;
      • always sanitizing user input;
      • using only in-bounds indices to access (dynamically allocated) arrays of the statically unknown size.