|
|
|
|
|
|
by matt_d
4084 days ago
|
|
|
> In general, any kind of analysis like the borrow checker will reject some valid programs, as it pays to be extra conservative. You then slowly expand the set of accepted programs, until hopefully, it matches the true set of valid programs, without accepting invalid ones. I'm wondering, is this possible in principle? Context: I'm thinking in terms of sound-and-decidable type-checking conservativeness [0], but perhaps that's a bad way of thinking about this? Perhaps borrow-checking is a special-enough case of type-checking that somehow isn't afflicted by this (how?) or gives up the soundness (does it?)? [0] "A sound type system with decidable type-checking (and possibly decidable type inference) must be conservative." -- http://gallium.inria.fr/~remy/mpri/cours1.pdf See also: https://books.google.com/books?id=7Uh8XGfJbEIC&pg=PA134 |
|
|