Wouldn't attribute macros (#[verus]) be more ergonomic than macro calls (verus! {})?

[KSXGitHub]

Instead of,

verus! {

fn foo(x: i32) -> (y: i32)
    ensures x < y
{
    x + 1
}

}

This looks better:

#[verus(x < foo)]
fn foo(x: i32) -> i32 {
    x + 1
}

Rustfmt and clippy also work better with functions with attribute macros than with a whole macro expression.

[Chris-Hawblitzel]

See #1297 and #1356 for discussion and implementation. Also see the ongoing discussion of Rust contracts at https://rust-lang.github.io/rust-project-goals/2024h2/Contracts-and-invariants.html .

[Chris-Hawblitzel]

Also see #1100 .

[KSXGitHub]

I only posted this question because the examples available only use verus! {}. Please consider improving or adding more examples.

[Chris-Hawblitzel]

Yes, that's a good point. I'm hoping to work on updating the documentation in the next couple months to incorporate more recent features like the attribute-based syntax.

[jaybosamiya-ms]

Brief note regarding the last line: we have verusfmt which supports formatting inside the verus! { ... } macro, and we have verus-analyzer which gives IDE support aware of verus! { ... } (and indeed adds other interesting features not in rust-analyzer). There isn't a clippy-equivalent (yet!).