Develop tools to rigorously study what programs mean.
Benefits
- Writing a PL-ish thing is inevitable
- Extensible systems, rich data structures, domain-specific languages (DSLs)
- Build skills with formalism and proof
- Precision, expressiveness, communication, clarity, confidence
- Become better programmers
- Travel to understand where you’re from!
Approach
- Develop the core of real languages
- include distinguishing features, omit sugar
- Start simple, extend w/ richer features
- develop reasoning techniques in parallel
- Discuss application to industrial PLs
- implement and prove to connect theory with code
Subgoals
- Develop tools for studying programs
- structural induction, inference rules
- Investigate core PL concepts
- types, functions, scope, mutation, iteration
- Learn how to use proof assistants
- powerful tools with increasing adoption