There's there is this little, really piddlingly small problem that TS isn't a sound language. Its type system, for convenience, pretends JS works in ways that are not how JS ACTUALLY works
You can of course slap a formal solver in without knowing that, which is evidently what this person did
Yes and no. TypeScript's type system is duck typing, but if you type absolutely everything it does closely describe actual JavaScript behavior. You can even set rules in your tsconfig file to forbid implicit null or undefined, but I don't do that in my own code.
> Acceptance proves, of the function's translation into the calculus, that for inputs and a heap meeting their declared types it does not get stuck and does not return a value outside its result type.
TypeScript's type-checker already proves the latter bit, no?
Actually it does not: if TypeScript says string, it does not mean string.
It could be number, or something else.
TypeScript tries to cover the most common scenarios, not all.
Looking at the README, it seems to have one. With strict on and noUncheckedIndexedAccess off, tsc is fine with this:
export function stale(xs: string[]): string {
const n = xs.length;
xs.pop();
return xs[n - 1];
}
You get undefined at runtime even though the signature says string. TScert won't take it unless you admit it in the return type, with string | undefined.
9 comments
[ 2.7 ms ] story [ 32.0 ms ] threadYou can of course slap a formal solver in without knowing that, which is evidently what this person did