I recently came across the notion that you need inductive data types (and can't just use Church encodings) if you want to do theorem proving, like proving that `0 != 1`.

I threw up some content up here: https://intellec7.notion.site/Drinking-SICP-hatorade-and-why... , along with an unrelated criticism of SICP.

I'd like to better understand what the limitations are of "everything is just a function".