News for hackers. Stuff that matters.

A comment on Translation of the Rust's core and alloc crates to Coq for formal verification. Parent comment

Re:Translation of the Rust's core and alloc crates to Coq fo... by Gajurgensen on Wednesday May 15, 2024 @02:23PM (#40370548)
Very interesting work! I'm curious how you handle loops/recursion? I imagine the `M` monad seen in the examples has a special primitive for loops?
[ Parent | on HN ]
Re:Translation of the Rust's core and alloc crates to Coq fo... by clarus on Wednesday May 15, 2024 @06:31PM (#40373203)
Yes there is a special primitive for loops in the monad. The primitives are uninterpreted, we define valid finite traces of execution of a program, and reason about these traces.

If a program has a loop we show that it terminates by constructing an execution trace. Note that we do not yet consider concurrency, so programs are deterministic.

[ Parent | on HN ]