Martin Escardo on Nostr: I, on the other hand, like using Agda as a blackboard for thinking, just like I like ...

I, on the other hand, like using Agda as a blackboard for thinking, just like I like using paper and pen for thinking.

I do believe that mathematics is inherently informal (and that ZFC, MLTT, ETCS etc. are not the ultimate answer to anything, but just distillation of what various people did informally in various different fronts).

This doesn't prevent me from both liking and finding formal mathematics with the aid of a computer useful (for myself - I am not advocating it would be useful for e.g. you).