> 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?
SSchick 1 hours ago [-]
I'd like examples/cases this catches that aren't handled by the existing compiler.
lupodevelop 1 hours ago [-]
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.
bazoom42 11 minutes ago [-]
But why not just enable noUncheckedIndexedAccess?
conartist6 4 hours ago [-]
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
austin-cheney 3 hours ago [-]
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.
evmar 2 hours ago [-]
The page talks about soundness in the second paragraph, not sure how you missed it.
conartist6 4 hours ago [-]
If you're interested I am happy to offer what I know on the topic but it won't be good news for you.
Basically if you want your project to survive and thrive you're going to have to implement a new programming language that runs using the semantics that Typescript claims to have rather than the semantics it actually has because it's Javascript under the hood.
I mean, if you want to despair, just try to account for the potential behavior Javascript Proxies could introduce in your Lean proofs.
If you do it correctly, Lean should tell you that virtually every Javascript program that has ever been written is possibly wrong, mostly for reasons that have to do with the lies Typescript tells about Javascript
lupodevelop 1 hours ago [-]
I think the docs cover this. They assume on purpose that the program never touches a proxy, so the proof only holds if that's true. To me that's the more interesting thing to argue about, what the proof assumes, not whether the author knows TS is unsound.
bazoom42 2 hours ago [-]
Can’t the type system reject code which undermines the soundness of the type system?
Rendered at 17:31:56 GMT+0000 (Coordinated Universal Time) with Vercel.
You can of course slap a formal solver in without knowing that, which is evidently what this person did
Basically if you want your project to survive and thrive you're going to have to implement a new programming language that runs using the semantics that Typescript claims to have rather than the semantics it actually has because it's Javascript under the hood.
I mean, if you want to despair, just try to account for the potential behavior Javascript Proxies could introduce in your Lean proofs.
If you do it correctly, Lean should tell you that virtually every Javascript program that has ever been written is possibly wrong, mostly for reasons that have to do with the lies Typescript tells about Javascript