Вот про доказательства свойств программ, да. Типы для этого предназначены. И информация о типе - сущность времени компиляции. А как оно в райнтайме будет представлено - дело третье. Там летают электроны туда-сюда и никаких типов нет.