Type Systems

• Statically typed vs dynamically typed
• Reasons for statically typed
  • Efficiency
  • Early bug detection
  • Enforce custom rules
• Reasons for dynamically typed
  • Flexibility
  • Metaprogramming
• Non-nullability
  • Billion Dollar Mistake
• Coq
  • Dependent typing
  • Types can represent any set of values
  • Type is actually a function that evaluates to true/false
  • Type checking a function means that it terminates and returns correct results
• TypeScript
  • Advanced type system
  • Unsound
• VeriFast
• Rust
  • Ownership