- the terms and types of the language
- the values (a subset of terms)
- the evaluation relation, telling you how you go from one term to the next
- the typing relation, telling you how you build well-typed terms and what their types are
- Progress states that if you have a well-typed term, it either is a value or it can take one step of evaluation
- Preservation states you that if you have a well-typed term of type T and it takes a step of evaluation, the resulting term still has type T
And we have the slogan, safety = progress + preservation.
I should also note that past a certain level of complexity of type system, you definitely would want to use a theorem prover such as Coq to formally verify and automate easy cases. The proofs themselves are actually quite boring (which is a good thing!).
It was surprising to me to discover how logical and mathematical Haskell’s type system is.
It’s the kind of topic that I’d probably not ever have thought about if I didn’t do a degree, but has had an impact on how I view other areas of computer science.
The first results of a Google search for "Amazon" are the company. Not the river.
The first results of a Google search for "Palantir" are the tech company. Not the fictional object from J.R.R. Tolkien's works it's inspired from.
And a Google search for "Rust" returns links to the programming language and the video game, before the chemical reaction.
If you want to search for things that exist, just add a Wikipedia quick search to your browser
The first results of a Google search for "C" are the programming language. Not the letter.
The first results of a Google search for "Python" are the programming language. Not the snake.