Non-understandable belief
© 2 Aug 2017 Luther Tychonievich
Licensed under Creative Commons: CC BY-NC-SA 3.0
other posts


Recent advances in automated theorem proving support my first postulate.


My second post in this blog was a postulate that most algorithms are outside the scope of computer science because even if they are created and proved correct, they still cannot be understood. In that post I raised an open question: “‍Do human-defined problems ever have only larger-than-mind-sized solutions?‍” Advances in automated theorem proving, brought to my attention by a recent article1 M. Heule and O. Kullman, “‍The Science of Brute Force‍” In CACM 60(8) pp. 70–79. August 2017. DOI:10.1145/107239 in Communications of the ACM do not address this postulate or its associated open questions directly, but they do provide related correct-but-incomprehensible results in another field.

Since I expect most of my readers have not taken a theory of computation course and thus will find that article a bit opaque, I will attempt a summary.

The above-summarized work addresses the understandability of proofs, not algorithms, but it does suggest that there are interesting problems with only incomprehensible solutions. While those problems are currently theorems and the solutions currently proofs, I don’t see any intrinsic reason why the same shouldn’t apply in other domains. The Frustrating Universe, where we can’t understand why a program works even if we know that it does, appears more probable now than it did when I postulated its existence six years ago.

Looking for comments…

Loading user comment form…