Reinventing Dafny from scratch: Keywords function, method, compiled, ghost, predicate, lemma

[MikaelMayer]

Let's launch this discussion: Some notes first

Mismatch with existing function affordances: Every new single Dafny user is being told that a "function" is a "mathematical function", that it is not compiled.
This is an unexpected behavior. It differs with every other programming language, where a function, whether a lambda, a top-level function like in JavaScript or PHP, are always compiled and accessible from procedures (global code or class methods)

Two languages that ressemble: There is a huge overlap between the "ghost language" (i.e. mathematical specification) and the "compiled language" (i.e. program expressions), and we know that if a function definition matches both languages, it can furthermore be embodied and become a "function method", for which PR #1555 suggests a new appropriate set of keywords "compiled function". It seems that the "ghost language" includes the language as well, except for lemmas where the state cannot be modified.

Given all this information, let's take a step back. Although "compiled function" is appropriate for future versions of Dafny 3, here is the current array of keywords.

Current state of the art

Type of lambda:	ghost without state modification	ghost with state modification	compiled
Statements:	lemma/colemma/greater lemma/inductive lemma	ghost method	method
1 expression:	function	N/A	function method / compiled function
1 expression returning bool:	predicate/copredicate/inductive predicate	N/A	predicate method / compiled predicate

We also acknowledge the useful feature of the almost "syntactic sugar:" below, where F_method is invoked at compile-time instead of F is every compiled context.

function F(a) requires R ensures E { X[a] } by method { P; return Z; }
<=>
function F(a) requires R ensures E { X[a] }
method F_method(a) requires R ensures F(a) {P; return Z; }

If we were to reinvent Dafny keywords from scratch, I would strongly suggest that the keywords "ghost" and "compiled" are present to enforce some behaviors, that "compiled" is the default for function, methods and predicates, with the special exception that functions and predicates can be inferred as ghost only.

But in any case, here is a suggestion of the keywords we might use, in bold for things that are a bit new. One idea is to keep the duality between compiled and ghost.

Proposal

Type of lambda:	ghost without state modification	ghost with state modification	compiled
Statements:	lemma/colemma/greater lemma/inductive lemma	ghost method | algorithm | proof	method | compiled algorithm | compiled proof
1 expression:	ghost function | expression | definition | def	N/A	function | compiled expression | compiled definition
1 expression returning bool:	ghost condition|ghost assertion | predicate/copredicate/inductive predicate	N/A	condition|assertion | compiled predicate

We could also have "procedure" instead of "method", but that's very minor.
Also, the language server should always suggest the simplest keyword, so if I prefix "function" with "ghost", it will suggest "expression" or "definition", but if I again prefix it with "compiled", it will suggest "function".

Now, the function .... by method would simply become expression ... by method, definition ... by method or ghost function ... by method or even definition .... by compiled algorithm..., whatever feels best (again, I would advise for the LS to suggest smallest keywords)

[smswz]

I think we should incorporate discussion about other places where ghost is used as well, for example ghost var.

Also, I think there should be a default modifier for methods, for example function is equivalent to compiled function similar to how protected is the default modifier in Java, but allows for it to be written to be explicit.

I would also like to say that as part of this discussion that there should be net fewer keywords as a result of the proposal. It is difficult to keep track of the various modifiers and a matrix explaining all of them is not intuitive and hard to develop fluency in.

[smswz]

I agree with that 100%. Something like lemma should be a shortcut and built on top of composable modifiers. Yes it'll probably never be used as ghost pure method, but for a developer it is easier to remember that than lemma is the intersection of 3 concepts, two of which have keywords and one of which is an inverse of a keyword (for example).

[robin-aws]

I would be careful with pure specifically, since it usually implies deterministic as well as side-effect free, and so far Dafny doesn't attempt to specify determinism with keywords.

[RustanLeino]

I agree we should avoid pure. Specification languages like JML have used "pure method" to mean a method that can be used in a specification. For a specification language like JML, which extends Java, it is natural to want to use the Java-library classes (like sets or sequences) in specifications, and to use those requires allocation. Therefore, it's hard to enforce being a "function" in Java, whereas "pure method" gives room for a wider interpretation. (See also equivalent-results methods.)

Dafny defines functions to be pure. Therefore, I think pure designation is superfluous (and confusing, since it suggests that some functions may not be pure).

[MikaelMayer]

Pure => StatePreserving?

[RustanLeino]

In JML (and something similar could have been said about the now defunct Spec#), "pure method" means it preserves the state of any previously allocated object. But a "pure method" is still allowed to allocate new objects (and to mutate the state of those new objects). This is a problem for two reasons. One reason is that, if the newly allocated reference is returned, then the "pure method" returns different results if you call it twice (which means it's not deterministic). Another reason is that even the allocation and mutations inside the pure method make it difficult to logically encode specifications that make use of the pure method.

[robin-aws]

I'm still personally mulling over how we might ideally encode all the different tasty flavours of Dafny procedures (if I may risk using one of the remaining terms we HAVEN'T used as a keyword yet :). But fundamentally, I'm starting to lean towards the principle that everything should be compiled by default, and ghost should be the one, consistent keyword we use to clearly indicate elements that are not present at runtime.

I suspect a decent number of current Dafny users are not going to like that (including @leino!), because it will make "pure" proofs in Dafny read a little less well and require a bit more typing. But here's my reasoning, which I'll propose as a Dafny language design tenant:

• Bias for programmers: Dafny is a programming language with a focus on verification. Dafny is NOT a proof assistant with a focus on executing code.

I'm hearing from lots of newer users of Dafny that it's just plain surprising that method definitions are compiled and yet functions are not by default. I assert that asking folks writing a lot of more advanced, non-computable specifications or independent proofs to add ghost more than they have to today is worth it if Dafny gets easier to learn, understand and reason about by its main audience. We could even have a switch to set the default behavior (which is likely how we'll navigate this breaking change anyway). I suspect there will be less need to add ghost than we might be worried about, as other keywords like the co in colemma and least/greatest already imply that something cannot be compiled anyway.

@MikaelMayer I had some thoughts around your particular proposed keywords, but I'll pause that for now as the wrench I'm throwing here probably forces a reset of our thoughts there anyway. :)

[cpitclaudel]

Python def are not deterministic (I'm not sure about Scala). If we want to rename, I think "function" could be come "specification"

[cpitclaudel]

But more importantly, do we have evidence that the names are hurting newcomers? Being surprised is not necessarily bad, if the surprise goes away quickly.

[RustanLeino]

The name function method causes everyone confusion. I guess we don't have any evidence that ghost function and ghost predicate would cause confusion or annoyance.

[kjx]

I hazard a guess that function method may be confusing because function is one thing with one syntax, and method is another thing with a different incompatible syntax.

So what's a function method? Who knows?

[keyboardDrummer]

Dafny 4 will change the syntax of function method to just function, while function will become ghost function. You can find more information in the documentation of the option --function-syntax: http://dafny.org/dafny/DafnyRef/DafnyRef#sec-controlling-language

[MikaelMayer]

My newest suggestion, to move the discussion since I still would like to go and accept #1555 :

In case functions are now compiled by default, and we encourage the use of "definition" instead of "ghost function", we would also change the following notation

function ... by method

to

definition ... by method

and emit a warning on function ... by method because function is normally already compiled and its body will be hidden by the provided method.

We do not no need to add the "compiled" keyword there, since it seems acceptable for most of us that methods are compiled.

[RustanLeino]

Thanks, everyone, for the good discussion. Based on it, and thinking it over for quite some time, my conclusion is the following (which is mostly what is already suggested above).

Let's start with a review of some concepts in Dafny.

Expressions and statements

Dafny distinguishes between expressions and statements. This is a frequent debate in programming languages, but for a verified language like Dafny, I think it makes good sense to keep this distinction. For example, it is desirable for specifications to be expressions. (If someone disagrees, then a debate on this topic is best done separately from the issue being discussed here.) Under this distinction, the body of a "function" is an expression and the body of a "method" is a list of statements.

So that expressions can be used in verification, they need to be deterministic. This means that an expression e == e, for any well-defined expression e, is always true. This is what Boogie and SMT2 expects. (Indeed, if you want to permit nondeterministic evaluation of expressions, you have to work quite hard and introduce all sorts of complications in the encoding.) Since a function's body is an expression, this means functions are deterministic (which in turn means that functions can be called from expressions). In contrast, statements (and thus also methods) in Dafny allow nondeterminism.

Compiled and not compiled

Dafny also provides a simple mechanism to omit certain declarations from an executable program. This mechanism is what is called "ghost". This mechanism would be useful in any programming language, and it is especially important in a verified language. For example, Dafny includes specifications, which are always ghost, and this means there is never any run-time overhead for specifications. Also, having ghost contexts in the language allows the language to support proof authoring, which in general may not be computable. Finally, having the notion of ghost expressions in the language lets ghost contexts use things that aren't easily computable or aren't computable in a finite amount of time, like Dafny's "least predicates", which in general are not computable, and two-state expressions, which would require storing arbitrary amounts of data if they were to be present at run time.

Declarations and keywords

Given these two distinctions--functions vs methods, and compiled vs not compiled--here is a table that shows Dafny's current keywords:

Kind of declaration	compiled	not compiled
variables/fields	var	ghost var
	const	ghost const
functions	function method	function
	predicate method	predicate
		twostate function
		twostate predicate
		least predicate
		greatest predicate
methods	method	ghost method
		lemma
		twostate lemma
		least lemma
		greatest lemma

Notes: A predicate is simply a function that returns a bool. All non-basic forms of functions and predicates as well as all forms of lemmas exist only in ghost form (see my comment above for motivating ghost constructs).

Here's what the same table would look like for Dafny 4, where 🆕 marks the changes from the current Dafny.

Kind of declaration	compiled	not compiled
variables/fields	var	ghost var
	const	ghost const
functions	function 🆕	ghost function 🆕
	predicate 🆕	ghost predicate 🆕
		twostate function
		twostate predicate
		least predicate
		greatest predicate
methods	method	ghost method
		lemma
		twostate lemma
		least lemma
		greatest lemma

Migration

As mentioned in the discussion above, it would be nice to provide some migration tools. Along those lines, but not necessarily as the only help for migration, we could (for a limited time, starting now and ending near the release of Dafny 4) offer a command-line option /functionSyntax:3 (for the first table above, and the default in Dafny 3) and /functionSyntax:4 (for the second table above, and the default in Dafny 4), and also support a migration mode /functionSyntax:migration, which would support the following:

Kind of declaration	compiled	not compiled
variables/fields	var	ghost var
	const	ghost const
functions	function method 🆕	ghost function 🆕
	predicate method 🆕	ghost predicate 🆕
		twostate function
		twostate predicate
		least predicate
		greatest predicate
methods	method	ghost method
		lemma
		twostate lemma
		least lemma
		greatest lemma

and would generate an error upon encountering a plain keyword function or predicate. Thus, to migrate code from the old syntax to the new, first use /functionSyntax:migration and fix all the errors by renaming function to ghost function and renaming predicate to ghost predicate. Then, use /functionSyntax:4 and fix all the errors by renaming function method to function and renaming predicate method to predicate.

Function by method

There is one more construct, which has been mentioned in the discussion above and has caused some confusion. It is the function-by-method construct. It has the form

function FunctionSignatureAndSpecification {
  Expr
} by method {
  StmtList
}

The whole point of this construct is to allow a function--which, remember, has the value of an expression, is deterministic, and does not make any allocations or changes in the heap--to be implemented by a list of (possibly nondeterministic, possibly allocating, possibly mutating) statements. The verification conditions associated with the function-by-method construct are such that any nondeterminism and heap use are unobservable to the caller of the function. This means that compiled code can use the StmtList instead of the Expr. Clearly, this is interesting only for compiled (non-ghost) code, so it's clear that StmtList must be non-ghost. Furthermore, since Expr is never going to be used in compiled code, the function-by-method construct might as well allow Expr to be a ghost expression. Thus, there's really only one form of the function-by-method construct.

So, then, should the syntax of function-by-method include a ghost keyword, as in

ghost function FunctionSignatureAndSpecification {
  Expr
} by method {
  StmtList
}

I think this would be confusing, because the initial ghost suggests that you can't call this function from compiled contexts. Instead, I think the syntax should remain the same in Dafny 4 as in Dafny 3, where you're invited to think of the

function FunctionSignatureAndSpecification { Expr }

part as all being part of the function's specification. The

by method { StmtList }

part is of concern only to the implementation, so the caller need not worry about it. Note that, under this view, the Dafny 4 keyword function (as opposed to ghost function) is indeed appropriate for the caller.

A previous proposal

In light of this more updated discussion and grander vision, I think we should cancel #1555.

[MikaelMayer]

Java's Predicate interfaces, although they have the same signature as our predicates (that is, functions that return Bools) are used in a VERY different context, filter Java streams. That's really the only use of these predicates in Java.

Our predicates' main usage is arguably to abstract over specifications that are naturally going to be erased at run-time. There are currently 3 extra types of predicates, and they all arise from the need to do verification. The concept of function, however, is that it will be available by default at run-time.

To ensure that verification is integrated with Dafny there should be only one keyword in the ghost world to express an abstraction that produces a boolean used in a verification context. I suggest to reuse predicate since it will least surprise Dafny users (nothing changes except for functions).

One thing that can be surprising if predicates are not ghost by default, is that it will trigger newcomers to think that specifications are not erased. I guess this is not a huge problem.

On the other side, I'm a proponent of later defining predicate type and it would be easier if predicates were compiled by default, so that we would get an error if the subtype test is not compilable (and need to add the ghost keyword in front of the predicate type)

[RustanLeino]

The one remaining issue,

• should there be both ghost and compiled predicates (keywords ghost predicate and predicate, respectively) or should there only be ghost predicates (keyword predicate)?

has bothered me for a while. On the one hand, it would be more uniform to allow both versions, just like both are allowed for functions. On the other hand, does anyone ever use predicate method today, and if not, wouldn't it be a nuisance to have to write ghost predicate for the overwhelming number of cases where today we can write just predicate?

From a pedagogical standpoint, I feel strongly that a predicate is just a function that returns a boolean value. That is, there's nothing inherently "ghost" or "specification only" about the use of the word "predicate". Dafny has some predicates that exist only in ghost form, namely twostate predicate, least predicate, and greatest predicate. But what makes these inherently ghost is not the use of "predicate", but instead the use of twostate, least, and greatest. These refer to a previous program state (twostate) and specify a fixpoint (least and greatest), so these are not realistic, ever, to provide in compiled code--having twostate in compiled code would be too expensive at run time, and computing fixpoints is at best inefficient (if nat is used to index the prefix predicates) or impossible (if ORDINAL is used to index the prefix predicates). Moreover, there is already a twostate function declaration, which for the same reason is always ghost. So, forbidding compiled predicates and using the sole keyword predicate for something ghost seems to invites more questions and confusion than allowing both ghost and compiled predicates.

There is one declaration in the language that consists of one keyword and is ghost-only, namely lemma. That seems fine, since a lemma is a mathematical thing, not something you'd ever expect to be computed at run time. (In other words, I see no reason to change the declaration of lemmas be always be ghost lemma.)

What started this entire thread was the confusion among all Dafny users that a function is ghost by default. I think we'll be making the same mistake again if we now will make predicate a declaration that introduces a ghost.

All of that said, I admit that the first thing that pops into my head when I think of a Dafny predicate is predicate Valid(), which stylistically is used to say that a data structure is in its expected state. By changing the polarity of ghost/compiled predicates, one will now have to write ghost predicate Valid() everywhere. Ugh. I thought I'd do some measurements to see how much of an issue this is.

There are 1579 uses of various kinds of predicates in the Dafny test suite, with the following breakdown:

occurrences	declaration
330	twostate predicate
108	least predicate
111	greatest predicate
111	predicate method
919	predicate

(Coincidentally, two of these counts are 111, and also 330 == 108+111+111. :O ) This table alone suggests that ghost predicates are far more common than compiled predicates. However, the test suite isn't the best representation of common code. For one, many tests are not specific to the ghost/compiled nature of declarations, so many such declarations may be using predicate over predicate method today, just because predicate is shorter.

A part of the test suite is the Dafny standard library. It is more representative of actual code. There are 25 predicates in this library, 2 compiled and 23 ghost. Looking at these in more detail, I found

occurrences	remark
12	necessarily ghost
7	could be compiled, by changing a type parameter from T to T(==)
4	could just as well have been compiled

If we make these changes, then we'd end up with

occurrences	declaration
13	compiled predicates
12	ghost predicates

This suggests that compiled predicates are in use and that we'd want to keep them (as declarations that somewhere say predicate rather than saying function ... : bool).

I looked at one more source of "good" programs, namely my book. Here is its breakdown of predicates:

occurrences	declaration
1	twostate predicate
19	predicate method
62	predicate

Of the 62 ghost predicates, 38 of them are Valid() predicates. These are all intended to be ghost (and many of them mention ghost variables, so they necessarily are ghost). Of the remaining 24 ghost predicates, 23 could just as well have been compiled. So, if those changes are made, then the book would contain

occurrences	declaration
1	twostate predicate
42 (19 + 23)	compiled predicates
39 (38 + 1)	ghost predicates

This shows that compiled predicates are useful in a significant number of cases. For these programs, a predicate is ghost pretty much iff it is a Valid() predicate, but there are many other predicates, too.

My conclusion, from the arguments and data above, is that Dafny version 4 should support both predicate (being compiled) and ghost predicate (being ghost) declarations, in parallel with function (compiled) and ghost function (ghost).

[cpitclaudel]

I find myself wondering often why the "ghost-ness" of an object is not inferred by the compiler. There would ghost predicate and executable predicate if one wants to be explicit, but writing just predicate would let the compiler infer. Incidentally, the same could apply to other places that are currently ghost-only: requires and ensures clauses, for example. f.requires() and f.ensures() would be ghost if the compilers infers that they need to be, and executable otherwise, unless the user specifies ghost requires and ghost ensures. Etc.

[atomb]

This could make it easier to temporarily evaluate more specifications at runtime, as well, without needing to change lots of annotations to make it work.

[MikaelMayer]

My conclusion, from the arguments and data above, is that Dafny version 4 should support both predicate (being compiled) and ghost predicate (being ghost) declarations, in parallel with function (compiled) and ghost function (ghost).

I support your conclusion now. Thanks for digging a lot.

I find myself wondering often why the "ghost-ness" of an object is not inferred by the compiler.

Ghostness is already inferred inside a method, but it cannot be inferred for accessible methods because otherwise a simple change could make a function or a predicate to disappear (suddenly it can be ghost!), which could break APIs relying on a (compiled) predicate.

[atomb]

I very much like @RustanLeino's proposal above. Would it make sense, on top of that, to allow ghost module? That would provide a convenient and clear way to separate specification from implementation. And it could be appealing to anyone who objects to writing ghost in front of every function. :)

[RustanLeino]

Yes, this is a possibility. What happens if you declare a type inside a ghost method? Types in Dafny don't have any ghost/compiled designation. Would types still be allowed, and would they be accessible to anyone outside the ghost module in the same way as they would have been from a module?

Btw, there is already an abstract module in Dafny. An abstract module is not compiled (and that includes any types it declares, too). However, an abstract module is allowed to be imported only by other abstract modules, which is probably not what you're hoping for. The only way to use an abstract module in a compiled setting is to declare a module that refines the abstract module, in which case the contents of the abstract module is, in essence, copy-and-pasted into the new module. But that does not achieve your hope of automatically ghosting everything, either.

[atomb]

Oh, that's an interesting question! One possibility might be that types declared in a ghost module could only be used by ghost code elsewhere. Why would you want that? I'm not 100% convinced that you would, but perhaps it would open the door for including types that couldn't be represented in an executable program but are useful for specification (infinite sets? other things?).