- 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!).
[0] https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf
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.
