Does anybody know of any languages that let you prove properties about the runtime of a function directly implemented in the language?
What is the difference? You are aware that the code is also only an abstraction, right?
The book that does the equivalent but with the properties checked at runtime is: Object Structures (like data structures but with objects).
Here is the link:
https://openlibrary.org/works/OL2979696W/Object_structures?e...
It really is more difficult to work with 'concrete implementations' to a degree that's fairly unintuitive if you haven't seen it first-hand.
To me it seems mandatory to work with some abstraction underneath that allows factoring a lot of different cases into a smaller set of possibilities that needs to be analysed.
It's also how we manage to think in a world where tiny little details do give you a likely insignificantly different world-state to think about.
What if the data is used for only a single lookup? For this case, actually a sequential search would have lower cost compared to sorting and binary search. Infact, sequential search may beat sorting and binary search for upto about 100 lookups. So I think it is important to consider overall cost.
Binary search talks about how long the search takes with this particular algorithm assuming the data is sorted. It does not talk at all about scenarios where the data is not sorted. In particular, it does not provide any views on costs without this assumption, let alone an incorrect one.
Yes, YOU need to consider when it is appropriate to use binary search. That is the case with all algorithms you will ever apply, and goes without saying.
