3 ms·
It's a nice read, an important topic, that of not trusting blindly formal proofs. No theorem ever applies to real world objects, it can only say facts about ide
by lapinot 3y ago
It's a nice read, an important topic, that of not trusting blindly formal proofs. No theorem ever applies to real world objects, it can only say facts about ideas. It's good to keep that in mind but at the same time that's all we got, it's like a basic premise of science. That's why it's important be able to also do testing and have executable models, to validate that the model behaves like you think it should. But it's also what serious people do already even when doing formal proofs. And it's also why there's usually a difference between scientifically "solving" something and the art of making it actually work.
- _flux 3y agoI've been practicing a bit TLA+ and one idea I've encountered—which I agree with— is: if we can't even get the idea to work, can we ever hope to get a working implementation? And similarly: if we have a good idea about how the idea works, then perhaps it is easy to end up with a good implementation. But the situation is of course completely different when you already have an implementation and you want to get "the simple idea" of how it works. And a lot of things you're going to interact with are those existing implementations, not just ideas of them.
- schoen 3y ago> No theorem ever applies to real world objects, it can only say facts about ideas. Einstein said something closely related: https://www.maa.org/press/periodicals/convergence/quotations-in-context-einstein https://www.maa.org/press/periodicals/convergence/quotations...