Also I just think that the whole way that the results of 0-CFA are represented by the types in a way such that type checking the code guarentees that the flow analysis was safe. We could talk about the trade off between having the types carry more information and having to make a new language for each pass. Maybe the latter is a bit too standard but I found it interesting.