4 ms·

The compiler does lifetime analysis, and there is a "reference borrowing" concept like in Rust.

• madgar 10y ago
  So it rejects code for which it can't prove lifetimes. Why not just say so? There's an uncomfortable degree of beating around the bush in this thread.
  • akavel 10y ago
    Curious if semantics of this subdomain of "allowed/legal" programs will be easy to understand, or will it be "try and see on case-by-case basis if your code compiles". Still, this way or the other, probably user will have to gradually learn and build intuition, as with learning any other aspect of any programming language. Also: will be/is the lifetime-checking done in the same way in the interpreter, even though it uses GC? Otherwise, those are in effect two, I think significantly different dialects of the language.
    • eriksvedang 10y ago
      It will require roughly the same amount of practice as when learning Rust, so a pretty significant learning effort I'm afraid. I'll try to do as much checking as possible in the interpreter so that the transition from interpreted to compiled code is smooth. Right now there is none though.
  • eudox 10y ago
    That's not quite how I'd put it. The documentation is pretty scarce, but if it's anything like Rust, you have to be explicit about ownership and somewhat explicit about lifetimes. That is, it's not just "rewrite your program until the prover succeeds".