comparison of OCaml and SML * SML has a formal Definition * SML has a number of compilers * OCaml has built-in support for oop comparison of OCaml and MLton * Performance o Both have excellent performance o MLton performs extensive WholeProgramOptimization, which provides improvements in modular programs o MLton uses native types, like 32-bit integers, without any penalty due to tagging or boxing. OCaml uses 31-bit integers with a penalty due to tagging, and 32-bit integers with a penalty due to boxing o MLton represents records compactly by reordering and packing the fields o In MLton, polymorphic and monomorphic code have the same performance o In MLton, module boundaries have no impact on performance * MLton's ForeignFunctionInterface is simpler * Tools o OCaml has a debugger, MLton does not. o OCaml supports separate compilation, MLton does not o OCaml compiles faster than MLton. o MLton supports profiling of both time and allocation
Metis is an automatic theorem prover for first order logic with equality. Features of Metis * Coded in Standard ML (SML), with an emphasis on keeping the code as simple as possible. * Compiled using MLton to give respectable performance on standard benchmarks. * Reads in problems in the standard .tptp file format of the TPTP problem set. * Outputs detailed proofs in TSTP format, where each proof step is one of 6 simple rules. * Outputs saturated clause sets when input problems are discovered to be unprovable. Project Status Metis is being actively developed