Provably-secure computing is a means by which you have a one-to-one mapping between your code and a proof that the results will not give you bad outcomes to a certain specification. The standard method is to implement a very simple language and prove that it works as a formal verifier, use this language to write a more complex formal verifying language, possibly recurse that, then use the final verifying language to write programs that specify start conditions and guarantee that given those conditions outcomes will be confined to a specified set.
It seems to be taken for granted on LW and within MIRI that this does not provide much value because we cannot trust the proofs to describe the actual effects of the programs, and therefore it's discounted entirely as a useful technique. I think it would substantially reduce the difficulty of the problem which needs to be solved for a fairly minor cost.
it's discounted entirely as a useful technique
I don't think it's true, that it's generally considered not useful. One of MIRIs interviews was with one person engaged into provably-secure computing and I didn't see any issues in that post. It's just that provably-secure computing is not enough when you don't have a good specification.
As per a recent comment this thread is meant to voice contrarian opinions, that is anything this community tends not to agree with. Thus I ask you to post your contrarian views and upvote anything you do not agree with based on personal beliefs. Spam and trolling still needs to be downvoted.