The Dafny compilation process translates Dafny programs into target language source code, in particular a .go file, compiles the result, and then potentially runs the result.

The Dafny-to-Go compiler writes out the translated files of a file A.dfy to a folder A-go/src. The -out option can be used to choose a different output folder. The file A.dfy is translated to A.go, which is placed in the output folder along with helper files. If more than one .dfy file is listed on the command-line, then the output folder name is taken from the first file, but just one .go file is written ithat combines the user source files, along with additional System and library .go files.

A multi-language program that combines Dafny and Go code “just” needs to be sure that the translated Dafny code fits in to the Go code. There are two aspects to this:

• ensuring that the names of entities in the translated Dafny code are usable from Go
• ensuring that the types are the same on both sides

The Dafny runtime library

The step of compiling Go files requires the Dafny runtime library. That library is automatically included in the output files if dafny is doing the compilation, but not if dafny is only doing translation.

Manually executing Dafny-generated Go code

Suppose a Dafny program is contained in a .dfy file, A.dfy, which containingthe Dafny Main method. One can build the corresponding Go program (without running it) using this command:

dafny build --target:go A.dfy

The compiled program is then executed using the command ./A or (cd A-go; GO111MODULE=auto GOPATH=\pwd` go run src/A.go)`

Alternatively the build and run steps can be combined: dafny run --target:go A.dfy

Combining Go and Dafny source files

The dafny tool is not yet able to automatically combined Go and Dafny source files.