Show HN: TypeScript as a proof assistant for intuitionistic propositional logic