YHK - yet another hacker news clone

TScert: A Sound Core for TypeScript

15 points bpierre 23 hours ago 2 comments

conartist6 19 minutes ago | parent

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

conartist6 8 minutes ago | parent

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