Thank you so much for taking the time to reply.

I now realized that I confused "syntactic" and "semantic" completeness.

I agree on your points; my first up there was ignoring a bit of the context (it was late...) and not meant to "motivate" the multitude of proof assistants by incompleteness theorem.

As a programming language person, I am quite convinced there will never, ever be an agreement on a common formal language (even if there was or is agreement on foundations it should be based upon) - it is the same as for programming languages.

This is more due to human nature rather than technical factors, and if we conceive logic as a linguistic activity, then we can see how foundations and the corresponding ergonomic language logic are related, maybe two sides of the same coin. "Foundations" in the context of mathematics appear (to me at least) as something technical and interchangeable.

Is there a venue for discussions on logics like these outside of the occasional logic-related HN threads? : )