> These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites.

and they all compile into the same fol/hol assembly (e.g. Isabelle translates its languages to fol and uses E for actual theorem proving, and E knows nothing about Isabelle language coolness), so in theory they should be able to integrate nicely.

My understanding is that the problem is they formalize in different mathematical foundations/axiomatic theories, but I am not an expert in this.