Language vision regarding safety guarantees

dlight:

It's making a check at runtime, but we need a check at compile time.

Sorry for the ambiguity in my post. Let's make things clear. Let's say you are author of library A, which has function foo. foo invokes bar in library B, and invokes unsafe function baz in library C. The safety requirement of baz comes from bar.

What I propose is that:

• If author of library B writes verified contract of bar, and the "ensures" contract of bar contains the safety requirement of baz:

Then author of library A does not need to do anything, just invoke bar and invoke baz. Everything is verified at compile time.

• If bar does not provide "ensures" contract that covers baz's safety requirement:

Then it's library A's author's responsibility to check it at runtime (which can make verification engine verify the safety requirement of baz).

dlight:

bar should depend on a very specific version of foo, like =1.2.3.

If things work as I proposed above, then it's needless to pin the version or vender it:

• If foo's author write verification contract, then if upgrading breaks, it is foo's author's responsibility
• If foo's author does not write verification contract, then bar should check it at runtime. Then upgrading will never be a problem.