Types and Programming Languages Chapter 8 Typed Arithmetic Expressions
As mentioned in the introduction of the book, we wish to check the run-time behaviour of a program without evaluating it in order to quickly spot potential bad behaviours. By introducing types into our language, we can express rules about those types (not entirely dissimilar to the evaluation rules we've seen in previous chapters) and check them statically before evaluating a program.
If we can prove that every well-typed term is either a value or can be evaluated a single step ("progress") and that evaluating a well-typed term also results in a well-typed term ("preservation") then we can confident that our program will not get stuck ("safety").
Cheersy cheers!
Thanks to Leo and Geckoboard for hosting, to all those who contributed snacks and to Abeer for organising the meeting (and last week's Computation Pub).