patricktree.me / overreacted
forked from danabra.mov/overreacted
my blog https://overreacted.io
fork atom

nng link

danabra.mov 06abdd12 41f132d4

+6
unified split
+6
public/beyond-booleans/index.md
··· 414 414 It turns out that the common logical operations we take for granted--`Or`, `And`, `Not` mentioned above, and so on, can be described as types containing values of other types, and functions between them. (Here's [an example in TypeScript](https://dev.to/yelouafi/types-as-propositions-in-typescript-2m97).) 415 415 416 416 Some of these ideas are almost a century old, and I'm excited to see them crop up in mainstream programming. I don't know how useful it is outside of maths but it's genuinely thrilling to pass facts around the program and to *know* they're true. 417 + 418 + --- 419 + 420 + ### P.S. 421 + 422 + (If this got you curious about Lean, go play the [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4)! At least for a few minutes. It's weirdly addictive, plus you already know how to solve [Level 0](https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/Tutorial/level/0).)