Verified Rust for low-level systems code

Re:Verified Rust for low-level systems code by IshKebab on Saturday May 04, 2024 @05:24PM (#40260396)

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?

[ Parent | on HN ]

Re:Verified Rust for low-level systems code by jaybosamiya on Saturday May 04, 2024 @06:20PM (#40260760)

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/

[ Parent | on HN ]

Re:Verified Rust for low-level systems code by tsujamin on Saturday May 04, 2024 @05:32PM (#40260449)

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

[ Parent | on HN ]