Did you mean EiffelStudio ? What was the painpoint at the time ?

I've only played with it 20+ years ago (a colleague was one of the few practitioner) and I don't remember EiffelStudio being _that_ terrible (it has a class browser that was not that much more horrible than Eclipse at the time) - but again, I only dabbled.

Now, I have to agree that the way they market the IDE as the best thing since bread came baked is kinda cringy..

That was due largely to the designers of the language, Bertrand Meyer and his wife, creating the tools. The tools, the seminars, and the books were primary income streams.

> Exactly the way you suggest, as an optional add-in

No, I don't suggest it, but criticize it. Rust performs its checking as a separate step after actual compilation, which sometimes leads to strange behavior (like borrow errors are shown only after actual compilation errors). I prefer an approach which is integrated with other language mechanisms.

> It's still WIP but in my side project I haven't found cases that can't be handled yet.

It's generally a good idea to write such an analyzer, but I doubt it can be useful without proper integration with the language itself (with huge semantics changes). If it's too strict, it will reject perfectly fine code, but otherwise it will catch only the most obvious errors and approve code having more complex memory bugs.

> In Rust variables are not destroyed after the last borrow ends but instead when it goes out of scope

That's the problem. Once I had a tricky case, where I locked a mutex in a match expression only to read a single field to match from the mutex contents. In one of branches of the match expression I locked this mutex once again and got a deadlock. Rust compiler wasn't smart enough to realize that the temporary variable for the mutex lock object should be destroyed earlier (it's no longer needed). So, I needed manually reading the field I need into a named variable to eliminate this deadlock.

A more advanced temporaries lifetime analysis would solve problems like described above, but it means basically duplicating a lot of stuff which is already done in the borrow checker (which runs as an afterpass).

Thanks!

So `items.[Iterable.iterator]()` is invoking a symbol-keyed method.

It's declared like:

    export interface Iterable<T> {
      static symbol iterator;

      [iterator](): Iterator<T>;
    }

    export MyArray<T> implements Iterable<T> {
      [Iterable.iterator]() { ... }
    }

I do want to add pure functions, especially for compile time constants. I want to add a macro system that can either run pure functions (on the AST or IR, not sure yet) at compile time, or run arbitrary code sandboxed in a Wasm module.

My idea was that with single pass, I can build SSA form during AST construction, and use phi-nodes to update type flow info. Then I could use SSA form to prove that I can use certain optimized bytecode instructions when a variable/register is known to be of certain type (I have virtual registers and fat instructions, eg ADD takes 2 sources and destination). Maybe I'm mixing control flow, type flow and SSA. I do not understand where I should stop with the pipeline if I use bytecode/VM.

The paper is: Brandis, Marc M., and Hanspeter Mössenböck. "Single-pass generation of static single-assignment form for structured languages." (https://bernsteinbear.com/assets/img/brandis-single-pass.pdf). It was quite understandable to me. For a deeper dive with proper SSA construction with dominance frontiers I could not find time to dig deeper, many other papers on SSA require focused CS work on them, not practically feasible for a side project. Also, single-pass is a requirement for very fast compilation to bytecode and LSP feedback.

I tried to read TS and Pyright source code, they share the same style of immense files and nested local functions, that was quite a steep wall to understand actual inner workings in detail. Maybe TS implementation in Go will be easier to read, it's on my later TODO list. It's tempting to use AI for help, but I'm quite experienced already with undoing AI work when it takes a wrong direction and I do not notice early.

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 of an SSA I guess!

Brandis, Marc M., and Hanspeter Mössenböck. "Single-pass generation of static single-assignment form for structured languages." (https://bernsteinbear.com/assets/img/brandis-single-pass.pdf).

Yes, added the expansion

HN does not use markdown code block formatting so this is hard to read. Formatting code blocks is simple, two blank spaces before any line to make it a code block and no need for extra newlines (unlike between paragraphs):

  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.

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

In D, the covariance/contravariance of contract inheritance is an important aspect of the contracts.

> Poor man's runtime "dynamic" version. AKA: A much worse version.

Contracts don't have to be evaluated dynamically, that's just one way they're implemented. See SPARK/Ada for an example of contracts being used to prove programs statically, not just test them dynamically.

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 took decades to get algebraic types or basic functional programming 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)

Adding them to languages not built around them also results in quite nasty boilerplate or runtime overhead which further discourage their usage.

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?

If LLMs are writing code, won't adoption progress on LLM-timescales? Humans would seem to be out of the equation.