Exactly. Types are the theorems, programs are the proof. So types are necessarily linked to programs. I think the author in the article has a misunderstanding of what types are