Rendered at 19:05:43 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
phtrivier 43 minutes ago [-]
For pedantry, should we note that design by contract came all the way from Eiffel ?
(But it's possible that even less people ever wrote Eiffel than D, so, who knows)
Panzerschrek 27 minutes ago [-]
> 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 be destroyed.
jeltz 2 minutes ago [-]
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.
buybackoff 33 minutes ago [-]
A genuine question: is the first point (flow typing / type narrowing) a subset of or intersection with or just an alias to SSA (static single assignment)? I'm playing with a small interpreted language implementation that is based on Lua, and have reached a point where I want to implement a single-pass SSA (there is a nice short CS paper on this), but cannot get my head around all the concepts, even if I need proper SSA for Typescript-like usability.
sebastianmestre 27 minutes ago [-]
SSA = static single assignment?
I am confused
buybackoff 15 minutes ago [-]
Yes, added the expansion
waldrews 20 minutes ago [-]
Completely free flow typing is risky in terms of interpretability, but type narrowing - var a : supertype; if (a is subtype) { // a is known to be subtype }, or type case, saves boilerplate in any OOP language.
diath 1 hours ago [-]
out (; balance == balance + amount) // checked after method returns
How exactly does it work? Is this a typo?
prydt 1 hours 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;
}
```
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 1 hours 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).
sick_of_slop 23 minutes ago [-]
Have there been any new good ideas in programming languages since LLMs came around? Or are we over that now..
joshmarinacci 21 minutes ago [-]
Programming language innovation is measured in decades. I expect LLMs will make it easier to prototype new concepts, but adoption will still progress on a human timescale
sick_of_slop 17 minutes ago [-]
The marketing pitch for these things was that they were supposed to induce "cambrian explosion of creations". That there was zero barrier to building anything anymore. This is surely true in programming languages especially, considering how fast LLMs took over software development? Surely this would mean we would get new ideas faster if that was the case? There is literally nothing stopping language designers from getting new concepts out there now even if nobody is using them in production yet.
> LLMs will make it easier to prototype new concepts,
So where are these prototypes?
ch4s3 57 minutes ago [-]
How does contract programming differ from refinement types?
prydt 49 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/
WalterBright 24 minutes ago [-]
In D, the covariance/contravariance of contract inheritance is an important aspect of the contracts.
bryanlarsen 52 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)
xorvoid 46 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 are a better solution.
aDyslecticCrow 6 minutes ago [-]
contract is way wider than simple refinement types. Refinement types are just a very specific group of invariants.
Contracts are an attempt to include formal specification languages into the implementation languages. You can enforce valid and invalid state changes, enforce relationships across the program state, or even enforce some level of correctness in behaviour.
> around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
That is completely not true. Plenty of dumb things prevail for faar too long for no other reason than momentum. Plenty of great things remain academic forever. It has decades to get algebraic types or basic functional programming to get somewhat accepted.
Design by contract is in theory a good idea but suffers from being a pain to use effectively. (making actually useful invariants that help the program more than an assert already would have)
jauntywundrkind 39 minutes ago [-]
I feel like languages are playing around different paints if coat mostly, and not trying to build more meaningful programming experiences.
I'd love to see a language whose pitch is that they have very next level stdlibs builtin. Effect for example is basically a mini stdlibs unto itself. It would be amazing to see such a principled deliberate craft applied to a language. Scope, layers etc etc etc etc: make visible, make first-class the actual pieces of computing, make them part of the language, explicitly modelled.
I'm also super excited for Zena, which just got announced yesterday! A typescript alike that compiles to wasm, and which really leans in to modern wasm, such as gc, wasi. A language that sits well at the cross-roads, that is excellent glue, that runs anywhere, that bridges other languages, is very compelling.
(But it's possible that even less people ever wrote Eiffel than D, so, who knows)
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 be destroyed.
I am confused
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
> LLMs will make it easier to prototype new concepts,
So where are these prototypes?
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/
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 are a better solution.
Contracts are an attempt to include formal specification languages into the implementation languages. You can enforce valid and invalid state changes, enforce relationships across the program state, or even enforce some level of correctness in behaviour.
> around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
That is completely not true. Plenty of dumb things prevail for faar too long for no other reason than momentum. Plenty of great things remain academic forever. It has decades to get algebraic types or basic functional programming to get somewhat accepted.
Design by contract is in theory a good idea but suffers from being a pain to use effectively. (making actually useful invariants that help the program more than an assert already would have)
I'd love to see a language whose pitch is that they have very next level stdlibs builtin. Effect for example is basically a mini stdlibs unto itself. It would be amazing to see such a principled deliberate craft applied to a language. Scope, layers etc etc etc etc: make visible, make first-class the actual pieces of computing, make them part of the language, explicitly modelled.
I'm also super excited for Zena, which just got announced yesterday! A typescript alike that compiles to wasm, and which really leans in to modern wasm, such as gc, wasi. A language that sits well at the cross-roads, that is excellent glue, that runs anywhere, that bridges other languages, is very compelling.