I thought the same thing, but they have a page that explains it pretty well — TypeScript v. Hegel

Turns out Hegel makes it a goal to be provably correct in respect to types, whereas TypeScript makes tradeoffs for productivity.

Hmm...

  const numbers: Array<number> = [];
  // HegelError: Type "Array<number>" is incompatible with type "Array<number | string>"
  const numbersOrStrings: Array<string | number> = numbers;

The very first example is already an odd choice, given that <number> is type-compatible with <string|number>. Errors should be flagged once we try to call functions on the elements, with calls on number[...] validated based on <number>, and calls on numbersOrStrings[...] validated based on the shared API between <string> and <number> (which is a tiny API surface, but there is one).

  numbersOrStrings[1] = "Hello, TypeError!";

Why is this not an error based on the incorrect assignment we already had? "HegelError: cannot assign to alias numberOfStrings of numbers, numbers is of type <number>".

  // HegelError: Property "toFixed" does not exist in "Number | undefined"
  numbers[1].toFixed(1);

Heck even this error is weird: we declared numbers as an array of <number>, not an array of <number|undefined>. If you're going to be that strict, track list sizes and go "HegelError: Property numbers[1] is undefined, which is type-incompatible with <number>".

It's because it is not proven that element with the index 1 exists. Even TypeScript enforces bounds checking these days.

As for the first one - as i understand, this will spoil the original array, as it is assigned by reference; so by writing the string into `numbersOrStrings`, you also write it into `numbers`, thus violating the type.

The benefit is right there in the line you quoted. TypeScript doesn't offer type safety at runtime, Hegel apparently does.

The line says no such thing, in fact it says the opposite. From the project page on GitHub, Hegel wants to have zero runtime type checking and have it all be proved statically at compile time.

You're reading type safety as type checking

Then what does "type safety at runtime" even mean? TypeScript is surely also type safe at runtime then, even if the type system is unsound: that is, after all, its whole value proposition.

Then maybe read the line again, because it very much does not say that =)