A few good ideas in programming languages
1–10 of 64 posts
Re: A few good ideas in programming languages
#2 out (; balance == balance + amount) // checked after method returns
Re: A few good ideas in programming languages
#3out (; balance == balance + amount) // checked after method returns How exactly does it work? Is this a typo?
I've never used D, but it appears to be valid syntax. https://dlang.org/spec/function.html#postconditions
Re: A few good ideas in programming languages
#4out (; 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!
Re: A few good ideas in programming languages
#5out (; balance == balance + amount) // checked after method returns How exactly does it work? Is this a typo?
I've never used D, but it appears to be valid syntax. https://dlang.org/spec/function.html#postconditions
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).
Re: A few good ideas in programming languages
#6out (; balance == balance + amount) // checked after method returns How exactly does it work? Is this a typo?
I've never used D, but it appears to be valid syntax. https://dlang.org/spec/function.html#postconditions
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.
Re: A few good ideas in programming languages
#7How does contract programming differ from refinement types?
Re: A few good ideas in programming languages
#8How does contract programming differ from refinement types?
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)
Re: A few good ideas in programming languages
#9How does contract programming differ from refinement types?
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/
Re: A few good ideas in programming languages
#10How 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.