A bit unfair. It verifies a subset of C because it is incomplete.
It looks as though the idea is that you can annotate existing code, which is a lot easier than rewriting.
It looks as though the idea is that you can annotate existing code, which is a lot easier than rewriting.
That's not necessarily true though.
Half decent C code already has a coherent memory management strategy. The problem is that humans can't follow even pretty straight-forward memory management strategies 100% of the time. If you have a function that returns memory the caller is required to free, or accepts a parameter that the function takes ownership of, that can be easily expressed but hard to get right every time.
In fact, functions typically document this... in half-decent C code. So we're really talking about formalizing the expression of memory management documentation that already exists and is already understood.
> And you're not getting as much safety bang for your buck for the effort as you would in a rewrite in actually safe language.
I just can't think of what the rational argument for this could be. A complete deep rewrite -- where the new language requires reorganizing the code at a low level so that a lot of existing logic cannot be reused (as-is, or transformed in certain specific ways) -- is extremely costly. It is on the order of the total cost of writing the software in the first place plus the entire cost already spent maintaining it over time. Some costs -- like the goodwill of users/adpoters -- simply cannot be paid again at the same rate. For large scale software there would be numerous regressions over a long period of time, while at the same time the software stops adding many new features, since all the focus will on the rewrite and bugs related to the rewrite. I will stand corrected if there is more than one or two exceptional cases of large scale software making a successful transition of this sort without paying a massive cost.
But rewriting assumes I learn a new language on top of rewriting.