= 27d567bc2d48d9f40e9ccc20ea370b15)
Perplexed comments on The Curve of Capability - Less Wrong
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 (264)
I see, it wasn't my intention to misquote you, I was simply not aware of a significant distinction.
By the way, has the checking of validity of a proof of code correctness to be validated or proven as well or is there some agreed limit to the depth of verification sufficient to be sure that if you run the code nothing unexpected will happen?
There are a couple of branches worth mentioning in the "meta-proof". One is the proof of correctness of the proof-checking software. I believe that fiddlemath is addressing this problem. The "specification" of the proof-checking software is essentially a presentation of an "inference system". The second is the proof of the soundness of the inference system with respect to the programming language and specification language. In principle, this is a task which is done once - when the languages are defined. The difficulty of this task is (AFAIK) roughly like that of a proof of cut-elimination - that is O(n^2) where n is the number of productions in the language grammars.