A few good ideas in programming languages

Post by Panzerschrek » Sat, Sep 12, 2026, 7:32 PM UTC

dnautics wrote: post #30

Panzerschrek wrote: post #14

> Borrow Checking It's very confusing name for this feature. It suggest that some sort of borrowing takes place and that it's just an optional check, which isn't the case. It should be named something like "enforced static usage analysis" instead. In my programming language I have similar mechanism. But it isn't just checking, since it affects code generation by tracking which variables are still in use and which can…

You can very likely borrow check in languages that don't have it in the type system. Exactly the way you suggest, as an optional add-in. It's still WIP but in my side project I haven't found cases that can't be handled yet. https://github.com/ityonemo/clr

Post by Panzerschrek » Sat, Sep 12, 2026, 7:38 PM UTC

jeltz wrote: post #23

Panzerschrek wrote: post #14

> Borrow Checking It's very confusing name for this feature. It suggest that some sort of borrowing takes place and that it's just an optional check, which isn't the case. It should be named something like "enforced static usage analysis" instead. In my programming language I have similar mechanism. But it isn't just checking, since it affects code generation by tracking which variables are still in use and which can…

In Rust variables are not destroyed after the last borrow ends but instead when it goes out of scope. I guess that is why it us called borrow checking.

Post by Jtsummers » Sat, Sep 12, 2026, 7:42 PM UTC

prydt wrote: post #4

diath wrote: post #2

out (; balance == balance + amount) // checked after method returns How exactly does it work? Is this a typo?

Looks like its a typo :( The correct way to go about this would be to return the new balance and capture the return value in the first part of the out postcondition like: ```D double deposit(double amount) in (amount > 0, "Deposit amount must be positive") out (result; result == balance) { balance += amount; return balance; } ``` My mistake! https://dlang.org/spec/function.html#postconditions

  double deposit(double amount)
    in (amount > 0, "Deposit amount must be positive")
    out (result; result == balance)
  {
    balance += amount;
    return balance;
  }

Post by Jtsummers » Sat, Sep 12, 2026, 7:45 PM UTC

xorvoid wrote: post #10

ch4s3 wrote: post #7

How does contract programming differ from refinement types?

Poor man's runtime "dynamic" version. AKA: A much worse version. In advanced cases, you'd need dependent types, but the only place where that almost shows up is in the "amount "Contracts" has been around a long time and has not caught on. That's usually a good sign that better approaches are prevailing. In other words: refinement types are a better solution.

Post by buybackoff » Sat, Sep 12, 2026, 7:47 PM UTC

mrkeen wrote: post #32

mrkeen wrote: post #29

Earlier quoted context omitted.

No. Type systems are unrelated to abstract machines which are unrelated to usability. Type inference/checking happens early in the pipeline. SSA is a way of laying out assembly instructions for an abstract machine. I say abstract because real machines re-assign values to the same addresses over time (which is precisely what 'single' static assignment prescribes against). Once you know which registers your real machin…

Ok. More thoughts. I was trying to see what was special about Crystal in this regard. It seems like if you took any ML or Haskell-like, you'd have type inference. Then you could allow shadowing (Rust-style) meaning the same symbol in the source code would be one variable now, and a different variable later. Then your compiler would need to distinguish x into x1 and x2 so it could track them separately. So yeah, kind…