Users should be able to annotate their unsafe functions with safety conditions and to differentiate between safety and panic freedom / correctness properties.

For example, the Index function index and the slice get_unchecked have the same pre-conditions, however, violating these conditions have very different consequences. Many users of index rely on the fact that it will panic if their assumptions about the index is incorrect. Thus, their contracts should reflect this difference.