Scott Aaronson's post is very interesting. Unfortunately, Scott's proofs in the above blog post do not work for strongly-typed foundations of Computer Science.

Scott Aaronson's post is very interesting. Unfortunately, Scott's proofs in the above blog post do not work for strongly-typed foundations of Computer Science. For more information, see the following: https://papers.ssrn.com/abstract=3418003 https://papers.ssrn.com/abstract=3418003