undefined | Better HN

0 pointsbluGill1y ago0 comments

Proofs are impossible in many cases because nobody really fully understands the requirements, they are sort of working them out as they go. (and in any case they will change over time). That might be what you meant by devilishly hard to write.

Tests let you instead say "with this setup here is what happens", and then ensure that whatever else you change you don't break that one thing.

To my knowledge nobody has scaled proofs to very large problems. I still think proofs should have a place in better code, but I can't figure out how to prove anything in my real world code base. (I could probably prove my languages basic containers - something that itself would be valuable!)

0 comments

Tainnor1y ago

> That might be what you meant by devilishly hard to write.

No, that's a separate problem. I agree that we don't always know what we need our code to do very precisely - although I think we could still increase the number of known invariants/properties in many situations - but even when you do, a proof is often hard to write.

Proofs also typically have the problem that they're not refactoring-proof: if you change the implementation of function f (but it still does the same thing), tests won't have to change, but a proof would have to be rewritten (the type would stay the same though).

dlahoda1y ago

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)

bluGillOP1y ago

> 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)

steveklabnik1y ago

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.)

j / k navigate · click thread line to collapse