Wandering Thoughts archives


Knowing things versus being able to prove them

Recently there has been a small contremps over how well (or not) IDEs can support refactoring for dynamic languages. To stereotype and condense, on one side are Java people who feel that without the guarantees provided by static typing, many sorts of automated refactorings are impossible to do reliably and so worthless; on the other side are Tim Bray and dynamic language people, who feel that various things can get them close enough, and besides there are a laundry list of situations where static languages don't have reliable refactorings either.

Recently I had a thought about the whole debate: one way to see it is in a conflict between knowing things and being able to prove them. In refactorings, the Java people want proof; Tim Bray and company are willing to settle for merely knowing things. And the heuristics and possibility for errors involved in merely knowing things give the Java people violent hives.

This also explains why the Java people don't see an equivalence between their refactoring imperfections and the dynamic language refactoring imperfections (something that irritates the dynamic language side of the debate a certain amount). The Java problem areas are already outside of what Java can prove, so people should already know that they're on their own in them in general; refactoring errors are just par for the course.

The difference between knowing things and being able to prove them also comes up a lot in computer security. A lot of security people are very hung up on the perfection of being able to prove things, and feel that anything less is not something that should be accepted.

programming/KnowledgeVersusProof written at 22:58:24; Add Comment

Page tools: See As Normal.
Login: Password:
Atom Syndication: Recent Pages, Recent Comments.

This dinky wiki is brought to you by the Insane Hackers Guild, Python sub-branch.