I think part of the assumption is that reflection can be bolted on trivially if the pattern matching is good enough. For example, consider guiding an SMT / automatic theorem prover by deep-learned heuristics, e.g. (https://arxiv.org/abs/1701.06972)[https://arxiv.org/abs/1701.06972] . We know how to express reflection in formal languages; we know how to train intuition for fuzzy stuff; me might learn how to train intuition for formal languages.
This is still borderline useless; but there is no reason, a priori, that such approached are doomed to fail. Especially since labels for training data are trivial (check the proof for correctness) and machine-discovered theorems / proofs can be added to the corpus.
I think part of the assumption is that reflection can be bolted on trivially if the pattern matching is good enough. For example, consider guiding an SMT / automatic theorem prover by deep-learned heuristics, e.g. (https://arxiv.org/abs/1701.06972)[https://arxiv.org/abs/1701.06972] . We know how to express reflection in formal languages; we know how to train intuition for fuzzy stuff; me might learn how to train intuition for formal languages.
This is still borderline useless; but there is no reason, a priori, that such approached are doomed to fail. Especially since labels for training data are trivial (check the proof for correctness) and machine-discovered theorems / proofs can be added to the corpus.