Dafny --no-verify doesn't speed up compilation of already verified programs

Dafny version

4.8.0

Code to produce this issue

No response

Command to run and resulting output

No response

What happened?

Dafny is roughly an order of magnitude slower at running small test programs (that are already verified) in comparison to a standard language like C#, C++, or C. The --no-verify option makes no discernible difference.

In certain problem domains such as video game development it is important to have a very fast edit-compile-run iteration cycle.

When using Dafny in VSCode, verification happens interactively, so if the program is already verified, it should be possible to hit a keystroke to rapidly run the program without waiting for a slow compilation.

Here are some measurements for a Hello World program on a fast desktop machine:

// hello.dfy
method Main() {
  print "Hello, World!\n";
}

Using the default C# backend:

PS C:\dev\dfy> ( Measure-Command { dafny run hello.dfy } ).TotalSeconds     
2.6343074

Using the Dafny Python backend is fastest, but still about 1 second. Here is a table of results with timings for the MS C++, C#, and C compilers for good measure:

Command                                 Time to run (seconds)
=============================================================
dafny run hello.dfy                                 2.6343074
dafny run -t py hello.dfy                           0.9621362
dafny run -t py --no-verify hello.dfy               0.9479757
cl hello.cpp                                        0.2219435
csc hello.cs                                        0.1298976
cl hello.c                                          0.0645671

Dafny is beautifully clean and elegant and should be able to compile and run fast as lightning if it skips the heavy SMT proof machinery. If nothing else, since Dafny can already interactively verify in VSCode, perhaps there can be a way to continuously compile in the background so that hitting "run" fires up the program instantly.

What type of operating system are you experiencing the problem on?

Windows

dafny-lang / dafny