Email me ice (facts) to contribute! Or suggestions on what to link to, for the facts I have below!

Here's what I have so far (vaguely in order of increasing obscurity):

- Lambda calculus is just a helpful syntax for writing proofs
- Parallelism is not concurrency
- People have been saying "Single-core scaling/Moore's law is over, the future is parallel programming" since at least the 1980s.
- Functional programming has been the future since at least 1978.
- Datatypes (e.g. product and sum types) can be defined just by using functions.
- Your computer is a distributed system
- Message passing is faster than shared memory
- a ≤ b means "a implies b"
- Something about quines?
- C's
`void`

should be called`unit`

, but at least they kept the same syntax for applying`f`

to`unit`

:`f()`

- The fixed point of
`option`

is the natural numbers. - Functions are codata.
- Pattern matching exhaustiveness checking is NP-hard.
- Partial evaluation gives you compilers for free
- Exception handlers are just dynamically scoped continuations
- All IO is monadic
- Dynamic languages are static languages
- Logic, programs, and category theory are the computational trinity
- Inheritance was invented to support intrusive lists and simplify GC implementation relative to composition
- call/cc is the computational interpretation of Pierce's law. (equivalently, double-negation-elimination, or the law of excluded middle)
- Contrapositive is function composition.
- Contraposition is CPS translation.
- cut is process spawning, id is delegation/forwarding.
- Fork is the law of excluded middle, and all continuations are delimited
- Delimited continuations are *mumble* polarity *mumble*
- Typeclass resolution is proof search
- Some surprising interpretation of coinduction/codata?
- Some surprising interpretation of effect systems/effect polymorphism?
- Some surprising interpretation of modal types?
- Some surprising interpretation of substructural type systems?
- Network packets/encryption are just values of an extensible type (search "channels are nothing but dynamic classes")
- You can prove there's no closed form for the 3-body problem by reducing the halting problem to it
- Microkernels are an abstraction inversion
- A mechanized proof of type-safety (preservation and progress) is an interpreter.
- You can do garbage collection without tags
- Garbage collection is just type inference.
- Tracing GC and refcounting are the same thing
- You can make a compacting memory allocator without moving pointers.
- Primitive datatypes are actually highly sophisticated universe-polymorphic type theory constructs
- You can pretty print functions without their source code.
- All computable functions are continuous
- Function equality is decidable (at some types)
- Mustard watches were first theorized in 1990 by Girard