I think it's possible that that's true, but am uncertain: the claim depends on formal methods for software construction that defy decompilation. But the higher-level the tools used for building software, the more effective decompilation tends to be. I also don't think we're even close to the apex of what decompilation (even of the clumsy, lossy compiled languages we have today) will be able to do.
So, it's an interesting question, and one I have much less of a strong opinion on.
If you can't tell, my real issue here is the idea that closed-source software is somehow unknowable. I know you're not claiming that it is. But I think if you look over these threads, you'll see that they tend to begin with people who do believe that, or claim to.
Let me try to advance a different thesis then: it is possible to write software in such a manner that the source code is amenable to methods of analysis that the object code is not. Accordingly, for software written in such manners, it is possible to provide certain guarantees if the source code is available for analysis, and those guarantees cannot be provided if the source code is not available. Would you agree with that?