With all due respect to Duncan... The reason why this is an issue at all is because the people who architected the internet were not thinking functionally. If they were, they would have come up with something like Nix.

But yes, interfacing between formally proven code and the wild wild West is always an issue. This is similar to when a person from a country with a strong legal system suddenly find themselves subject to the rule of the jungle.

The better question to ask is why did we choose to build a chaotic jungle and how do we get out of it