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".
replies(3):