Verus: Verified Rust for low-level systems code

Re:Verus: Verified Rust for low-level systems code by sangel on Wednesday April 23, 2025 @09:20AM (#43771843)

Obviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish.

This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enumerate all X.

[ Parent | on HN ]

Re:Verus: Verified Rust for low-level systems code by stephencanon on Wednesday April 23, 2025 @04:03PM (#43776103)

Indeed. Exhaustively testing a 64b input space requires about 600 machine years for each nanosecond that the function under test takes to run. So, _very_ short-running critical functions are testable on a cluster, but not efficiently testable, and if a function is simple enough to be testable, then it's usually easier to prove that it's correct instead.

[ Parent | on HN ]