F* vs. Dafny

[YaakovDavis]

They seem quite similar.

How are they related? What are the similarities/dissimilarities?
What types of problems will be easy to tackle in one language, while hard on the other?

Thanks,

[nikswamy]

They are similar superficially, inasmuch as they are both languages designed with verification in mind and they both use SMT solving technology.

But, there are many differences:

F* is a higher order programming language in the ML tradition; Dafny is a first order imperative language in the style of Pascal (although some higher order support is coming in Dafny)

F* has a dependently typed higher-order logic; Dafny uses a non-dependent first-order logic.

F* has refinement types which are useful for stating invariants; Dafny does not (although some initial work on that has begun).

F* has inductive type families useful for constructive proofs; Dafny has simple datatypes only.

F* has no IDE support yet; Dafny has a very nice IDE in Visual Studio.

F* has no coinduction; Dafny supports coinduction.

F* is customizable by user-defined effects; Dafny is not.

F* is available on multiple platforms; Dafny requires .NET.

F* has no special support for object-oriented programming; Dafny provides object oriented constructs.

...

This list is by no means exhaustive. But, I hope it gives you a general sense of what's available and not available in the two languages.

I may add to and/or refine this list.

[YaakovDavis]

Thanks for the detailed explanation.

How are refinement types in F* different than pre- and post-conditions (requires/ensures) in Dafny?
I'm new to both languages, and probably from a novice level, they appear to me as serving the same verification end.

Edit:
Also, Dafny does seem to support higher order functions:
http://research.microsoft.com/en-us/um/people/leino/papers/krml243.html#sec-function-types

[catalin-hritcu]

Top-level refinements on function argument and result types serve indeed the same purpose as pre- and post- conditions. In F* the two styles (refinements and pre- and post- conditions on functions) are possible and equivalent by subtyping.

However, quoting our recent ICFP submission:

Refinement types are more than just a notational convenience:
nested refinements within types can be used to specify properties
of unbounded data structures, and other invariants. For example,
the type list nat describes a list whose elements are all non-negative
integers, and the type ref nat describes a heap reference that always
contains a non-negative integer.

I think that in theory one might be able replace even nested refinements with pre- and post- conditions by turning all values into functions at all levels (remember that we only have pre- and post- conditions on functions). This kind of encoding would, however, be extremely inefficient and inconvenient in practice.

[YaakovDavis]

Thanks, Catalin. I now understand the difference.

Can you address my remark about higher-order logic?
Do you see any difference between the languages?

[catalin-hritcu]

I don't know that much about Dafny, but adding higher-order functions to Pascal will probably not turn it into ML :)

[nikswamy]

Dafny recently added higher-order, heap-reading functions.

Higher orderness is pervasive in F*. You can write higher order pure functions (which you cannot in Dafny), as well as higher order functions with arbitrary effects. You can specify properties in higher order logic, etc.