[firechickenbird]

At this point I'm wondering if the TypeScript type system can be used for dependant types that would allow formal verification of the programs

[remexre]

That'd require it to be sound and programs to be total: an infinite loop is a proof of anything, and type system unsoundness leads to false proofs