> A lack of understanding about the data lifetimes in a program means lack of understanding about the data. But this argument can extend forever. Is your prog

> A lack of understanding about the data lifetimes in a program means lack of understanding about the data. But this argument can extend forever. Is your program precisely dependently typed? If not is that a lack of understanding about the nature of the data as well and should you challenge yourself to fix that? You have to trade-off how much you specify things with how valuable it is to get the result more quickly.