Starting with "That's nice" is extremely flippant and is an immediate turn off to any subsequent statement. A stronger opening to discredit the [..] proposal would be to take the closing quote "We've been doing that with D for over 20 years" and point out that storing the length of an array of a certain type is a specialization to arrays of dependent typing that has been around since Howard and de Bruijn extended lambda calculus to match predicate logic by creating types for dependent functions and pairs. Each axis of the lambda cube is another source of nondeterminism that has to be reasoned with and languages that explicitly exclude said functionality for simplicity can point to as justification for such restrictions.
I didn't say D invented it, so no need to discredit it. I said D has been using it for 20 years and proves it works famously with C style pointers and arrays.
And no claim was made about what D invented. Continuous use does not prevent door latch bushings from disintegrating; How long some thing has been used for is not proof that the replacement will work.
Fat pointers are a purely value level construct. STLC alone covers that. Non-determinism isn't really related to the lambda cube, even CoC is deterministic.
A pointer type is understood "to point" at a memory address with no restriction on being stack allocated. CoC is ambiguous as many different versions of the theory of constructions have been formulated that are not all equivalent and not necessarily bounded & deterministic.
