[dlahoda]

i am coming from rust. writing a lot of narrowing wrappers/type states/proptests/const and runtime asserts/expects of possible proofs. i am targeting to do these first.

for big things wiring many things together, will use normal tests(given lean4 allows to reflect on io graph, i guess can have some fun here too)

[bluGill]

> runtime asserts/expects

Those are not proofs. If you have a formal proof tool (I'm not aware of one for rust, but there is a lot of progress in this area) they feed and and sometimes tools can prove things. Though beware, there are limitations to this approach - sometimes they would have to solve the halting problem to say code is correct (though if they say code is wrong they are right), other times the problem is solvable only on a computer that doesn't exist yet.

Types and const are a form of formal proof - if you don't cast those away (I'm not sure what rust allows, particularly in unsafe). However there is a lot more potential in formal proofs. Rust's borrow checker is formal proof, and there are safe things you might want to do that the borrow checker doesn't allow because if it was allowed rust could no longer prove your code memory safe (a trade off that is probably worth it in most cases)

[steveklabnik]

I agree with what you're saying, but some context:

> I'm not aware of one for rust, but there is a lot of progress in this area

https://github.com/model-checking/kani is probably the best known one, I believe there are a few others.

> (I'm not sure what rust allows, particularly in unsafe).

You can't "cast const away" in Rust, even in unsafe. That is, you can do it in unsafe, but it is always undefined behavior to do so. (I am speaking about &T and &mut T here, const T and mut T exist and you're allowed to cast between those, as they have no real aliasing requirements and are really just a lint.)