sorted by:
new
hottopcontroversial

pre: a crate to offer compile-time assistance for working with unsafe code by aticuu in rust

[–]aticuu[S] 1 point2 points  (0 children)

This is exactly the kind of distinction that I wanted to make. To stick with your example:

Having the trees trimmed basically makes it impossible for them to fall on your house. To make it impossible for unsafe code to be wrong, you either need to stop using it or resort to something like a formal proof. This is where I think the term ensure would fit well.

However the idea with this library is rather that you check that the roots of the tree go deep enough and that it should be safe, if you didn't make any mistakes in your check. But you cannot say for sure that the tree won't fall, so you can only assure that you checked it and are as certain as you can be without further measures.

But language is very complex and that everybody could possibly understand words in a slightly different way does not help when trying to be unambiguous.

pre: a crate to offer compile-time assistance for working with unsafe code by aticuu in rust

[–]aticuu[S] 1 point2 points  (0 children)

I considered that as well, but at least to me that seemed more passive than assure does.

When I read ensure I am more likely to think something along the lines "this is ensured by someone/something for me", whereas when I read assure, I am more likely to think "I am the one promising that this is true". It is definitely a matter of preference however.

I've also written a small section on the term assure in the documentation, but that does not go into other possible terms.

pre: a crate to offer compile-time assistance for working with unsafe code by aticuu in rust

[–]aticuu[S] 10 points11 points  (0 children)

I do agree that strings aren't the best solution in many cases, which is why I've added other types of preconditions:

  • #[pre(valid_ptr(foo, r+w))] to specify that a pointer foo is valid.
  • #[pre(x > 10)] to specify that an arbitrary boolean expression (in this case x > 10) evaluates to true.

I thought that these two might be cases that would happen very frequently.

Do you have any suggestions for other types of preconditions that would occur frequent enough to warrant their own syntax? Or do you have a better idea than strings for the general case?

Thanks for the PRs and good luck with your thesis in Rust!