I rather read some thing that's formal and readable, than just merely readable.

> One thing I would be interested in is an objective look of how the limitations of computation affect formalized mathematics. I think there’s a lot of sticky computational and philosophical problems there that I don’t see mentioned a lot.

~Goëdel~ Gödel's theorems are not relevant. Consider even if the halting problem had the other answer, it still could be impractical to do the brute force search. Same thing here.

And frankly, the formal methods community is sick of people spreading FUD from that stuff. Mixing romantic humanism with technical misunderstandings is no good.