4 ms·
Is it guaranteed that Rust -> WhyML -> Rust Would ever yield a fixed point?
by rowanG077 4y ago
Is it guaranteed that Rust -> WhyML -> Rust Would ever yield a fixed point?
- thesz 4y agoIt is possible to produce a dump of Rust program AST into WhyML datatypes and/or functions and project and prove what can be proven. The structure of WhyML datatypes and functions can be parsed and transpiled back into Rust.
- Jweb_Guru 4y agoIn theory no. In practice probably (Rust compiles itself to a fixed point from older versions in around 3 iterations, IIRC).