[bpolverini]

That would be really cool, but I think enforcing that is undecidable. My gut tells me that having that language feature at compile time is the same as the Halting Problem.

[nostrademons]

In its full generality it's undecidable, but there are probably restrictions you can build into the type system to make it decidable. I was thinking something along these lines:

  class Symbol {
    @init(constructor) originalToken: Token
    @init(constructor) position: SourceLocation
    @init(Parser.parse) scope: SymbolTable
    @init(Parser.parse) declaredType: Type
    @init(TypeChecker.typecheck) inferredType: Type
    @init(DataFlowAnalyzer.computeLiveness) usages: List<Expr>
  }

And then the type system carries an extra bit of information around for whether a reference is fully-constructed or not, much like const-correctness. Fields marked with @init can only be written on a reference that's not fully-constructed. There's no compile-time enforcement for initialization order, though it'd be pretty easy to do this at runtime (convert them to null-checks or special not-initialized sentinel values). Newly-created references start out with the "initializing" bit set, but once they're returned from a function or passed into a function not in the list of legal accessors, they lose this bit unless explicitly declared.

It's basically the same way "mutable" works (in languages that support it), but with a separate state bit in the type system and extra access checks within the mutating functions to make sure they only touch the fields they're declared to touch. You can fake this now by passing mutable references into initialization functions and then only using const, but it's a bit less specific because many classes are designed to be long-term mutable through 1-2 specific public APIs but also need to be mutated internally for deferred initialization, and lumping these use-cases together means that deferred fields can be touched by the public API.

[tgflynn]

I suspect that the ideal language (at least for human use) is one that is just shy of Turing completeness. Once a program compiles and an initial configuration phase has passed all loops would be bounded and all recursions would be guaranteed to terminate. Except for the case of programs that aren't supposed to terminate for which there would be a single construct allowing wrapping everything inside one and only one infinite loop.