On Mon, Jul 21, 2014 at 12:10 PM, Jonathan S. Shapiro <[email protected]> wrote: > On Sun, Jul 20, 2014 at 11:43 PM, Matt Oliveri <[email protected]> wrote: >> >> For >> deductive systems, "complete" means that a statement is provable >> whenever it's true in all models. This is the closest idea I know to >> what I'm getting at: that a program has a type whenever* its compiled >> code has the required properties... >> >> * Gödel's incompleteness theorems make this impossible in interesting >> cases, so we'll settle for almost complete. > > Ah. I may now understand what you mean by "complete". Completeness in the > sense of Gödel is not a goal for a programming language. We're not trying to > do a general logic system for proving arbitrary properties. We're trying to > discharge limited properties (e.g. no dynamic errors) over a limited problem > domain.
Statically ruling out dynamic vector range errors in a Turing-complete language should already run into Gödel's incompleteness in principle. Unless you know some incredible trick. But in practice no one runs into problems with Gödel's incompleteness. That's why I'm ignoring the issue. The completeness I want is not the opposite of Gödel's incompleteness. _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
