# [fit] **Write tests**
---
# [fit] **Thank you** for
# [fit] attending my **Tim** Talk
---
# [fit] Write **txxxs**
---
# [fit] Feed
# [fit] back
---
# [fit] Write fewer
# [fit] **Runtime tests**
^ Possibly fewer tests
^ Will show techniques to reduce the scope of what needs to be runtime tested
^ In some cases for things are hard to or nearly impossible to test otherwise

---
# [fit] Write more
# [fit] Compile-time
# [fit] **types**
^ Types can be a form of testing, proving that the code does what you think it does

---
# [fit] Rule of **least power**
# [fit] 
# [fit] 
# [fit] 
# [fit] **Parse**, don't validate
# [fit] 
# [fit] 
# [fit] 
# [fit] Make **impossible**
# [fit] states **impossible**
---
# [fit] **[Curry-Howard](https://en.wikipedia.org/wiki/Curry–Howard_correspondence)**
# [fit] Correspondence
^ A direct relationship between computer programs and mathematical proofs
^ Pictures and bios of Curry and Howard
^ Give a little explaination of your passion for mathematical thinking

---
## [fit] **Intuitionistic Logic**
## [fit] ≅
## [fit] **Typed Lambda Calculus**
---
## [fit] **Logic**
## [fit] ≅
## [fit] **Types**
---
# [fit] **Curry-Howard**
| Logic | Types |
| --- | --- |
| propositions | types |
| proofs | terms |
| proof of proposition A  | inhabitation of type A |
| implication | function type |
| conjunction | product type |
| disjunction | sum type |
| falsity | void type (empty) |
| truth | unit type (singleton) |
---
# [fit] **Propositions**
# [fit] as **types**
---
# [fit] **proofs**
# [fit] as **programs**
---
# [fit] **normalization of proofs**
# [fit] as **evaluation of programs**
---
# [fit] **Curry-Howard**
| Logic | Types |
| --- | --- |
| propositions | types |
| proofs | terms |
| **proof of proposition A** | **inhabitation of type A** |
| implication | function type |
| conjunction | product type |
| disjunction | sum type |
| falsity | void type (empty) |
| truth | unit type (singleton) |
^ It's enough to have an instance (inhabitant) of a type to prove it

---
# [fit] **Curry-Howard**
| Logic | Types |
| --- | --- |
| propositions | types |
| proofs | terms |
| proof of proposition A | inhabitation of type A |
| **implication** | **function type** |
| conjunction | product type |
| disjunction | sum type |
| falsity | void type (empty) |
| truth | unit type (singleton) |
---
# [fit] **implication**
# [fit] a → b
# [fit] **if a then b**
---
# [fit] [Rule of **least power**](https://en.wikipedia.org/wiki/Rule_of_least_power)
---
# [fit] [**Parse**, don't validate](https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate)
---
# [fit] [Make **impossible** states **impossible**](https://www.youtube.com/watch?v=IcgmSRJHu_8)
---
# [fit] Rule of **least power**
---
# [fit] **Parse**, don't validate
---
# [fit] **Parsing?**
---
# [fit] Turning **nebulous** data
# [fit] into **structured** data
---
```typescript
const head = (i: Array<a>): a = {...}
```
---
```typescript
const head = (i: Array<a>): Maybe<a> = {...}
```
---
```typescript
export interface None {
  readonly _tag: 'None'
}

export interface Some<A> {
  readonly _tag: 'Some'
  readonly value: A
}

export type Maybe<A> = None | Some<A>
```
---
# [fit] Make **impossible** states **impossible**
---
# [fit] Red, Green, Refactor
---
# [fit] Red, Green, Refactor
| Red | Green | Refactor |
| Types | Implementation | Refactor |
---
# [fit] Type Driven Development?
---
# [fit] Pragmatism
---
# [fit] Notes
* **Ideally all examples are real code examples from GitHub**
* Names are not type safety examples?
    > https://github.com/chaturangalagama/clinic-manager/blob/b650ebb50ac3f4e467c578f5ba28fb9cf545a3d7/src/app/objects/response/PatientRegistryListResponse.ts
* Impossible states examples?
    *