A Few Good Ideas in Programming Languages

(prydt.xyz)

36 points | by airhangerf15 5 hours ago

2 comments

  • ch4s3 13 minutes ago
    How does contract programming differ from refinement types?
    • xorvoid 2 minutes ago
      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 <= balance" assertions. That's also silly because if you typed "amount" and "balance" correctly, then "balance -= amount" has to produce a runtime error because the resulting balance would be negative and not a valid value for the type. So, it's a very natural place anyway to force the programmer to properly handle errors anyways.

      "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.

    • prydt 5 minutes ago
      The contract programming in D is pretty much syntactic sugar for placing asserts at different parts of your program.

      Refinement types can be used as compile time checks for preconditions and postconditions, while this contract programming is inserting runtime checks.

      Here's a good post on the type state pattern in Rust (we don't actually have refinement types in something like Rust but the type state pattern is somewhere closer to refinement types on this spectrum): https://cliffle.com/blog/rust-typestate/

    • bryanlarsen 8 minutes ago
      The various contract proposals for Rust are used as input to both formal verification tools as well as input to the optimizer. A good example of one such tool that could utilize contracts is cargo-anneal (https://crates.io/crates/cargo-anneal)
  • diath 33 minutes ago

        out (; balance == balance + amount) // checked after method returns
    
    How exactly does it work? Is this a typo?
    • prydt 20 minutes ago
      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

    • lgas 23 minutes ago
      I've never used D, but it appears to be valid syntax. https://dlang.org/spec/function.html#postconditions
      • diath 19 minutes ago
        I'm not asking about the syntax, I'm asking about the logic where a value can be equal to itself plus another value when the pre-condition is that it must be > 0.
      • prydt 19 minutes ago
        The syntax is correct but I made a logical error since balance is being compared to itself (as opposed to the new balance at the end).