Outstanding issues with Dafny test support

[robin-aws]

From #447:

• Reject programs that use {:test} incorrectly before attempting to compile them (must be "static", must return a "result type", etc.)
• Explicitly report the lack of support in the other target languages
• Backfill documentation
• Define minimal requirements for {:test} semantics, in order to specify correctness for translation to each target language. I'd propose that there must at least exist a command that provides a non-zero exit code IFF at least one {:test} method returns a result for which IsFailure() returns true.
• Provide CLI switches for running tests using the target language tooling? Something like dafny /test?
• Create a mechanism for customizing the compiler per language? It would be better not to reference specific libraries in the compiler itself.

[robin-aws]

Removed bullet on special-casing modifies - Main() is not special-cased, methods with {:main} are, and I don't think we want that here anyway.

[MikaelMayer]

Where are we on this issue? Is it just a documentation issue or a feature/enhancement?

[robin-aws]

It's a mix of a bunch of different issues really, just a brain dump from when I first added the attribute. :) I'll split it up and perhaps knock off the easy documentation tasks with a quick PR.