3 ms·
Write tests for your C code. Run c2rust (mechanical translation), including the tests. Let a LLM/MCTS/verifier loop go to town. Verifier here means it passes co
by the8472 2y ago
Write tests for your C code. Run c2rust (mechanical translation), including the tests. Let a LLM/MCTS/verifier loop go to town. Verifier here means it passes compiler checks, tests, santiziers and miri.
Additional training data can be generated by running mrustc or by inlining unsafe code (from std/core/leaf crates) into safe code and running semantics-preserving mechanical refactorings on the code.
This can be closer to AlphaProof than ChatGPT
- astrange 2y agoYou could already use ASAN + UBSan, or Frama-C.
- the8472 2y agoI did mention using sanitizers in the verification step of the optimization loop. The optimization goal here would be reducing the lines of `unsafe` while preserving program semantics.
- TestingWithEdd 2y agoEssentially neural program synthesis