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

full

danabra.mov 41f132d4 fca19b7b

+1 -1
public/beyond-booleans/12.svg public/beyond-booleans/12-full.svg
+1 -1
public/beyond-booleans/index.md
··· 407 407 408 408 Now you can see the whole picture: 409 409 410 - ![Same picture, but with 2 + 2 = 4 and 2 + 2 = 5 included. Types are Eq 2 2 and Eq 2+2 4, while values are Eq.rfl 2 and Eq.rfl 4](./12.svg) 410 + ![Same picture, but with 2 + 2 = 4 and 2 + 2 = 5 included. Types are Eq 2 2 and Eq 2+2 4, while values are Eq.rfl 2 and Eq.rfl 4](./12-full.svg) 411 411 412 412 Proofs are values of types of propositions, and each proposition is typed in a way that it is only possible to construct a proof when that proposition is correct. That's how mathematics can be bridged to programming--not by computing numbers, but by computing logic itself--from which you can construct numbers and more. 413 413