Typescript types
Solving puzzles
Proving facts of programs
Basics Of Typescript
Intro
- Typescript - Javascript + Types
- Types are present only in compile time
- Complete type erasure after compilation
Basics Of Typescript
Generics
- Strong typing Array, Promise and other common higher order structures
- Opens up gateway to type level recursion
Basics Of Typescript
Assertions
- Sometimes types need stronger clues
- With the base rules set, assertions can take care of runtime validations
Logical Programming
Solving simple puzzles
- Encode facts in structural types
- Populate the base data
- Let the type system do its magic!
Proving properties of programs
Type level arithmetics
- Defining Numerals using generics
- Defining operators using recursion
Proving properties of program
State machine encoding in type level!
Shhh... Dependent Types in disguise
Proving properties of program
Template literals
Proving properties of program
Typelevel lexers & parsers!
How does type level programming work
Type system - A minimal functional language in itself
- Generics are type level functions
- Functions i.e Generics compose easily
- And hence we encode any data using Church encoding - Making typescript's type system a mini lambda calculus**
Implication & future of programming
Formal verfication, Open source & testing
- Properties of programs verified by compilers - Formal verification & Theorem provers
- Scanning through large open source code bases for backdoors
- Test driven development suddenly mainstream ??
- And, proof driven development becomes the hip
Implication & future of programming
Spec oriented programming
- Types seem to be the dual of imperativeness**
- Types feel like teaching to a toddler about a domain**
- Specifications can be encoded at type level
- And provers can generate a proof - where one of them could be our correct program
Implication & future of programming
- Correctness - From hospitals to flights
- The next bank or a country's constitution could be only programs
- Bureaucratic machines can be replaced by (self amendment) programs**
- And so, taking chances is never an option...
Thanks
Inspiration & Regards
Thanks
Inspiration & Regards
