Типобезопасность (англ. type safety) — свойство языка программирования, характеризующее безопасность и надёжность в применении его системы типов.
Система типов называется безопасной (англ. safe) или надёжной (англ. sound), если в программах, прошедших проверку согласования типов (англ. well-typed programs или well-formed programs), исключена возможность возникновения ошибок согласования типов во время выполнения[1][2][3][4][5][6].
Ошибка согласования типов или ошибка типизации (англ. type error) — несогласованность типов компонентов выражений в программе, например попытка использовать целое число в роли функции[7]. Пропущенные ошибки согласования типов на этапе выполнения могут приводить к багам и даже крахам программ. Безопасность языка не является синонимом полного отсутствия багов, но, по меньшей мере, они становятся исследуемы в рамках семантики языка (формальной или неформальной)[8].
Надёжные системы типов также называют сильными (англ. strong)[1][2], но трактовка этого термина часто смягчается, кроме того, его часто применяют к языкам, осуществляющим динамическую проверку согласования типов (сильная и слабая типизация).
Иногда безопасность рассматривается как свойство конкретной программы, а не языка, на котором она написана — по той причине, что некоторые типобезопасные языки разрешают обойти или нарушить систему типов, если программист практикует скудную типобезопасность. Распространено мнение, что такие возможности на практике оказываются необходимостью, но это вымысел[9]. Понятие о «безопасности программы» важно в том смысле, что реализация безопасного языка сама может быть небезопасной. Раскрутка компилятора решает эту проблему, обеспечивая языку безопасность не только в теории, но и на практике.
Робину Милнеру принадлежит выражение «Программы, прошедшие проверку типов, не могут „сбиться с пути истинного“»[10].
Иначе говоря, безопасная система типов предотвращает заведомо ошибочные операции, связанные с неверными типами. Например, выражение 3 / "Hello, World" очевидно является ошибочным, поскольку арифметика не определяет операцию деления числа на строку. Формально, безопасность означает гарантию того, что значение любого выражения, прошедшего проверку типов, и имеющего тип τ, является истинным элементом множества значений τ, то есть будет лежать в границах диапазона значений, допустимого статическим типом этого выражения. На самом деле, в этом требовании есть нюансы — см. подтипы и полиморфизм для сложных случаев.