3 ms·
I think you're missing his point. He does acknowledge that statements of facts and their proofs can be easily communicated, but claims that the understanding th
by robryk 3y ago
I think you're missing his point. He does acknowledge that statements of facts and their proofs can be easily communicated, but claims that the understanding their discovery was a side effect of cannot be communicated easily. This is not affected by having a better way to express facts and their proofs.
- ke88y 3y agoNo, I get his point. I think the transmission of knowledge and insight and clarity works very differently for executable artifacts than for artifacts written in natural language. > This is not affected by having a better way to express facts and their proofs. But it is if those expressions are possible to interact with and use through not only conceptual abstraction but also procedural abstraction. With good proof automation? Maybe you can interact and play with ideas through many layers of automation-enabled abstraction. Maybe you have a tactic or ATP procedure that uses a lemma in clever ways without you even knowing it exists, and only after building on that edifice for years do you bother to dig in and understand what the proof automation is even using. Mind you: not what the lemma means or how it's proven or the underlying historical development of ideas, but that it even exists. Maybe you never dig in and realize it exists. Maybe you use these new theorems and proofs -- discovered only through extremely essential and clever use of a critical lemma you don't even know that you are using -- to do something useful in the world. That can't happen today; not really. It would take very powerful proof automation for this world to exist. Code and books are very different things.