Jon Sterling on Nostr: Proof assistants invert the "abstract" and the "concrete" in my experience. What ...

Proof assistants invert the "abstract" and the "concrete" in my experience. What seems more abstract when working on paper tends to be extremely concrete when working in the proof assistant. This is related to the comment of nprofile1qy2hwumn8ghj7un9d3shjtnyd968gmewwp6kyqpqez3yya8tpgge7lk4jq2zxz0cj3d2mcgev9mffd4ec7tfy84hre4skst6k2 (nprofile…t6k2) a while back that somehow formal proof is more informal than informal proof... (Hope I'm not getting that wrong)