> Knowing absolutely nothing about formal verification Are you sure about that? That is what we've been talking about all along. After all, the thing that sepa

> Knowing absolutely nothing about formal verification Are you sure about that? That is what we've been talking about all along. After all, the thing that separates Rust from Python, with respect to our discussion here — the thing that allows code to be less fragile, is its type system. Which is formal verification! Rust is very limited in that regard, not allowing verification of much, but still very much lives on the formal verification spectrum. The trouble when you can't verify much is that you end up in a situation where something like: fn add(a: i32, b: i32) -> i32 { a + b + 1 } Is able to compile just fine despite being completely wrong. To deal with that you need to write tests (which is essentially runtime formal verification). But once you've written the tests, you've also largely covered the properties that are statically verified, leaving no real benefit to LLMs. But I infer that you aren't writing tests either, and that Rust's type system is feeling advantageous as it at least provides some limited verification. You seem to be enjoying that workflow, which is why I mentioned that there are languages with way better types systems that you might enjoy even more. There are probably hundreds of languages between Rust and full verification on the spectrum, so if Rocq isn't the exact one for you, try some others! They're only a prompt away.