Kind2 as a Rust transpiler.

[omrischwarz]

Hi, all. I'm trying to use Kind2 as part of a Simulink compiler pipelines. The steps would be

1. CoCoSim to turn Simulink into Lustre.
2. Kind2 to convert to Rust
3. Cargo to compile.

I'm working in a space where Kind2's verification capabilities would be nice to have but are not really in anyone's radar. On the other hand, Simulink wrapped with C comes with memory problems and data races, and putting Rust in the compile chain instead of C would be wonderful, as it would verify the absence of those.

How much of th current work in this project is heading in that direction? I've no OCaml experience so it would be some time before I could offer my own help.

[daniel-larraz]

We currently lack the resources to dedicate to that feature, but contributions are welcome.