@Feryll "... there are indeed propositions in base Coq for which neither it nor its negation has a witness" That too is at least an understatement: indeed, there are undecidable propositions in classical mathematics, too, so that is more misleading than it is just off mark...

"To not deny is to assert" I think is already a better characterization. I don't mean a holy war, indeed I only said yours was an understatement: IMO that is a critical point though, maybe even a crucial one, as for understanding what is what. -- Anyway, just an observation/remark on that specific point, indeed I have no qualms with your answer overall.

@PeterLeFanuLumsdaine Generally speaking, if I have to dig into a library's implementation details in order to use it, then the library is not good enough... Encapsulation is a name for this.

"classical logic ... destroys hopes to have well-behaved computation" is the least of the problems with classical logic and quite and understatement...

Conversely, one might argue that Turing Machines are not an adequate model of computation: indeed there is no such thing as a machine that does not halt or crash or gets switched off, eventually.

I have decided to mark this answer as a solution: I have found every answer and every comment very useful, thanks very much again to all those who have contributed, just, since I can accept one and only one answer, this is the one that eventually I find nearest to the desiderata in my original question.

Thank you, very interesting. Indeed, already what is happening in run_inv, how you concretely achieve that kind of "partiality", is totally new to me... I will certainly read more about this Braga method.

(2/2) So, this solution quite makes sense to me, it is just a bit more concrete-level than I'd wish/hope: analogous to formalizing a discourse on arbitrary (unbounded) precision arithmetic with a multi-precision (hard-limited) specification... OTOH, please correct me if I am mistaken, a fuel-based approach makes an IsFinRun fully decidable and effective, so I would end up needing that ingredient at some stage anyway, to the point that I might very well introduce it since specification time... -- Need to think more about it/play more with it. Thanks very much for now.

(1/2) We have no way to guess the amount of fuel needed, to the point that, to preserve correctness, instead of option I'd try and use a three-valued result as in Some, None, Failed (equiv., an option of option), and parametrise the whole thing on a global hard depth limit: which I'd say is a common pattern in resource constrained environments. (Would you agree with this "reading"?)

Thanks very much @NaïmFavier . This indeed works: Definition IsFinRun (r : run) : Set := {p : pos | r = pos_to_run p}. -- OTOH, I had thought about the coproduct, but then I thought, maybe wrongly, that it would be less elegant than structural subtyping as well as less faithful to the informal progression and notions... anyway, as for decidability, I'd have thought working in Set was the critical factor: I am missing the distinction you are making in that sense.