Compile time vs. Verification time vs. Runtime

[ePaul]

In the language specification it is not clearly mentioned that there are three phases, and how they depend on each other.

This is what I gathered (e.g. from the description of the assert and assume and fail statements):

• Compile time is when the compiler parses and analyzes the source code, does some type checking, and emits code suitable for verification and for running.
• Verification time is when a verifier takes the compiled code (maybe in a different representation than the one which is run) and checks that it actually does what it pretends to do.
• Run time is when an interpreter takes the compiled code and executes it.

I first assumed those phased happen always in this order, and only verified code is actually run. But the description of fail tells me that it throws a fault at runtime, while the verifier makes sure it is not reachable. How can it then throw a fault? Same for assert (which is basically if (! condition): fail).

Does this mean verification is optional?

[DavePearce]

Hey Paulo,

Yes, verification is optional (at least at the moment).

Also, it does say this in the glossary:

• compile time The point in time at which a given compilation group is compiled into binary form.

It doesn't mention runtime or verification time though. It's not clear what should be said here. It might be too specific given the nature of modern compilers (e.g. incremental compilation, etc).