Interesting! Looks most similar to Creusot. The syntax is definitely nicer but w... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		IshKebab on May 4, 2024 \| parent \| context \| favorite \| on: Verified Rust for low-level systems code Interesting! Looks most similar to Creusot. The syntax is definitely nicer but wrapping your entire code in a macro surely is going to upset rust-analyzer?

jaybosamiya on May 4, 2024 | [–]

A fork of rust-analyzer, called verus-analyzer, provides support for Verus syntax and actions (including new proof-specific actions) https://github.com/verus-lang/verus-analyzer/

tsujamin on May 4, 2024 | [–]

I’m not sure how rust-analyser works, but presumably you’d make the macro a no-op and just return the original tokens in debug builds

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact