Can you say more clearly what it is that you're saying follows from the Curry-Howard Correspondence? My understanding is that the proof that your program is is

Can you say more clearly what it is that you're saying follows from the Curry-Howard Correspondence? My understanding is that the proof that your program is isomorphic to is not necessarily a proof of anything interesting in the domain of your program, which means that the practical consequences of Curry-Howard for day to day programmers is pretty limited. This is very definitely the case for most type systems practically used today (including the one that typescript uses).