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.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
