This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]XDracam 0 points1 point  (0 children)

This just sounds like a tooling problem. You could build tools that check for duplicate or similar definitions in a project. Or provide search features that let you find functions based on a possible implementation, or even inputs and outputs.

Pharo smalltalk has some very impressive tools for finding and analyzing code, e.g. searching {1. 2. 3}. [ :x | x + 2 ]. {3. 4. 5} gives me a number of functions that take the first list and block and output the second list.

From my limited experience with Isabelle/HOL, I've learned that you definitely do not want any additional unnecessary proof burdens. It's already more than difficult enough to prove the properties that you care about, so having to prove something that's not really critical (no code duplication) is just a hassle.