# Glossary

- anonymous type: A type built from its interpretation, thus without syntax.
- associated proof: An associated constant of the proof type.
- bottom type: The type with an empty interpretation.
- permissions to use: Characteristic of a robust type.
- promised type: The type at the end of a borrow of a mutable reference.
- restrictions to use: Characteristic of an unsafe type.
- robust type: An anonymous type missing some safe values.
- safe type: A Rust type (its interpretation is exactly the safe values).
- safe value: A value satisfying the safety invariant.
- soundness: The property of type systems that only accept defined programs.
- subtyping: The inclusion relation between type interpretations.
- type interpretation: A mapping from types to their set of values.
- unsafe type: An anonymous type containing some unsafe values.
- unsafe value: A valid but not safe value.
- valid value: A value satisfying the validity invariant.
- value: A part of the execution of a program.
- variance: Type-level functions behavior regarding subtyping.