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.
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.
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.
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.