10
$\begingroup$

I know that the definition of Standard ML has been mechanized in Twelf, but are there tools which allow me to verify my Standard ML code satisfies certain properties or specifications?

I'm vaguely aware Don Syme had done some proof-of-concept work on this in the '90s, e.g., with:

  • Syme, Donald. "Reasoning with the formal definition of Standard ML in HOL." In HOL Users' Group Workshop, pp. 43-60. Springer, Berlin, Heidelberg, 1993.

But is there some HOL or Coq (or whatever) library which lets me prove results about my code using the language definition? Like, something I can tangibly get ahold of and use right now (rather than some paper reporting some proof-of-concept trial balloons). I'll even settle for working with a "purely functional" fragment of SML.

I'm also aware of Harper's book Software Foundations which seems more general than what I'd like.

I am aware of CakeML, but it looks intractable unless you are a developer working on it. And, as I understand it, CakeML is developing its own "ML dialect" rather than adhering to Standard ML (correct me if I am wrong).

Improve this question
$\endgroup$

1 Answer 1

Reset to default
2
$\begingroup$

See also, VanInwegen and Gunter’s HOL-ML paper (also from the 90s), doi: 10.1007/3-540-57826-9_125.

I think the people who have done this would agree that working with the formal definition as printed is extremely arduous. (As per Andreas Rossberg’s Defects in SML it’s also known to be faulty.) Given this, no-one is keen on the linked idea of proving that the definition is equivalent to another, more tractable specification. All told, I think it's fair to say that you really do have little choice but to pick something you think is “good enough” and work with that instead.

If you want to be as close as possible to SML, then CakeML is best. (There are semantic differences, but they're not huge.) If you want to verify programs in a functional programming language you can often get away with proving properties of functions expressed in the proof assistant's logic. But if you want to get down to the level of references, pattern-matching and exceptions, you will need a deep embedding of a real language, and not many of those have accompanying compilers...

Improve this answer
$\endgroup$
4
  • $\begingroup$ Thanks for the HOL-ML reference (I wouldn't be surprised if there were a few more papers out there, somewhere). I'm not defending the definition of SML; I'm more interested in verified programming with SML. It sounds like CakeML is the way to go, as it's the closest thing to what I'm interested in, but...well, it seems very "heavy weight". $\endgroup$
    – Alex Nelson
    Commented Feb 14, 2022 at 2:31
  • $\begingroup$ Real languages are heavy, sadly. That's why people prefer to prove theorems of mathematical functions and then "export" those functions as code. In CakeML we also prefer this route where possible! (We export to CakeML in a proved/verified way, and then run the compiler on that.) $\endgroup$
    – Michael Norrish
    Commented Feb 14, 2022 at 6:32
  • $\begingroup$ I was hoping Standard ML was lean enough to cheat this fate! But I suspect you may be correct, and my hopes were in vain. Out of curiosity, does CakeML export SML code? Or does it compile to machine code? $\endgroup$
    – Alex Nelson
    Commented Feb 14, 2022 at 18:08
  • 2
    $\begingroup$ If you start with a mathematical function in HOL, it’s a two-stage process. 1. You use the verifying translator to produce CakeML abstract syntax. 2. You compile the AST to machine code using the verified compiler. If you already have a CakeML program, you only do step 2. $\endgroup$
    – Michael Norrish
    Commented Feb 14, 2022 at 22:52

Not the answer you're looking for? Browse other questions tagged or ask your own question.