Типобезпечність
властивість мови програмування, яка характеризує безпеку та надійність у застосуванні її системи типів / З Вікіпедії, безкоштовно encyclopedia
Типобезпечність (англ. type safety) — властивість мови програмування, яка характеризує безпеку та надійність у застосуванні її системи типів.
Систему типів називають безпечною (англ. safe) або надійною (англ. sound), якщо у програмах, які пройшли перевірку узгодження типів (англ. well-typed programs або well-formed programs), виключено можливість виникнення помилок узгодження типів під час виконання[en][1][2][3][4][5][6].
Помилка узгодження типів або помилка типізації (англ. type error) — неузгодженість типів компонентів виразів у програмі, наприклад спроба використати ціле число як функцію[7]. Пропущені помилки узгодження типів на етапі виконання можуть спричиняти баги і навіть креші програм. Безпека мови не є синонімом повної відсутності багів, але щонайменше вони стають досліджуваними в рамках семантики мови (формальної або неформальної)[8].
Надійні системи типів також називають сильними (англ. strong)[1][2], але трактування цього терміна часто пом'якшують, крім того, його часто застосовують до мов, які здійснюють динамічну перевірку узгодження типів (сильна та слабка типізація).
Іноді безпечність розглядають як властивість конкретної програми, а не мови, якою її написано — тому що деякі типобезпечні мови дозволяють обійти або порушити систему типів, якщо програміст практикує мізерну типобезпеку. Поширена думка, що такі можливості на практиці є необхідними, але це вигадка[9]. Поняття про «безпечність програми» є важливим у тому сенсі, що реалізація безпечної мови сама може бути небезпечною. Розкрутка компілятора вирішує цю проблему, забезпечуючи мові безпечність не лише в теорії, але й на практиці.