Hacker News Reader

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

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