favour an attribute style procedural macros

[gilescope]

Having the code inside macro! { code here } generally is bad for IDEs, code formatting etc.
If at all possible switch to #[macro( { ensure .... })] fn ....

Everyone generally does it this way at first and then regrets it and switches. Just hoping to fasttrack you.

[utaal]

Moved to discussion (expand for details).

Hi @gilescope, thank you for the input. I'll move this to a discussion, as we generally use issues for actionable bugs, and discussions for feature requests and design / language design discussions (see the [README](https://github.com/verus-lang/verus/blob/main/README.md), no worries though, I'm happy to move things around when necessary).

Thank you for the input! This is something we have discussed from the beginning of the project -- as you're saying there is a trade-off between tool support and the ability to precisely control the language. Verus is designed (primarily) for verifying full-functional correctness of full programs (although it can be used to verify simpler properties), and our experience doing the same with other tools (like Dafny) is that one has to write a significant amount of specification code and annotations (see https://github.com/verus-lang/verus/blob/main/source/rust_verify/example/nevd_script.rs for a small example of verifying a function returning the nth fibonacci number in Verus, or https://github.com/achreto/verified-node-replication/blob/main/verified-node-replication/src/exec/rwlock.rs for part of the verification of a reader-writer lock in a larger project).

We try and keep the amount of annotation needed low, and we have seen shorter proofs than in other tools, but this kind of reasoning still requires a bunch of annotations: our experience suggests that we (and our users) probably wouldn't want to wrap all of them in local macros, and having full custom syntax significantly aids readability. The cost is significant, as you say, but we have not regretted the choice so far. That said, we have talked about providing an alternative syntax based on attributes for projects for which it's more challenging to adopt the verus! macro, or that only verify simpler properties than full correctness, where annotations would be more lightweight.

In terms of formatting support, there's been some excellent work by @jaybosamiya, @parno, and others to write a formatter for Verus, verusfmt: https://github.com/verus-lang/verusfmt, which we've adopted to format e.g. the Verus standard library (vstd). There is also a fork of rust-analyzer, called verus-analyzer, with support for Verus syntax: https://github.com/verus-lang/verus-analyzer (there's been a lot of recent work on it, but I haven't used it in anger yet -- but I do see the value of tool support, rust-analyzer is a significant productivity boost for me while developing Verus itself).