= 27d567bc2d48d9f40e9ccc20ea370b15)
somnicule comments on What are your contrarian views? - Less Wrong Discussion
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (806)
I'm not sure what you mean by provably-secure, care to elaborate?
It sounds like it might possibly be required and is certainly not sufficient.
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.