This mindset is literally the way safe programs work. What do you think functions are?
This isn't some 100k line long program where this function is used all over the place and code churns constantly so checking invariants in the function definition makes sense.
It could use `str*` functions without any issues then. Nul-terminated strings are perfectly safe with assumptions to follow.
Anecdote: I fixed 3 reported segfaults and another 2 after fuzz-testing in a small 500 line lib. Original author had the same cowboy mindset about keeping all stuff in his head. It's always last words before getting into CVE database.
Good code consists of easy to use abstractions. In general Chris's blog is dedicated to poking bad abstractions and giving good examples. `substring` is objectively bad.
You (and other commentators) literally arguing that keeping staff in the head or making some documentation or notes or forcing yourself or others check low level implementation details are better than making one trivial fix and forget about it. I find it really amusing.
Good code consists of solving a problem simply and efficiently. You can have a great program which is concrete. Abstraction is a tool for managing complexity, not a goal.
I would really encourage writing a large program C or assembly, as a practice of how to deal with programming problems without immediately wrapping things in an interface. A lot of things that feel like producitivity end up being wastes of time.
It is simple, short and obviously correct. You don't have to record every single line of reasoning in a proof or argument, when the intermediate steps are obvious. Same applies here. It isn't necessary to document this because it is obvious from a glance that it is correct. You can derive its correctness with a moment's thought. So it is fine not to assert it - that would be clutter.
While it is "obvious" that it is correct, it is, in fact, neither obvious nor correct if A. you ever subtract from then len field, and B. you use "len != 0" as a check for "is string non-empty". This program does both things quite a lot and it requires a conscious check to re-assure yourself that no, in this particular program, the patterns of acitons A (subtractions from the len field) never break the property B (non-zero len means that the string is not empty). But any minor modification may accidentally break this harmony if you are not aware that it is required to hold.
This isn't some 100k line long program where this function is used all over the place and code churns constantly so checking invariants in the function definition makes sense.
It is called in one (1) place in a small program.