Обсуждение:Типобезопасность

Браво!

Хорошая статья. Конечно, лучше указать источники на фразу о С++ (памятуя о другом обсуждении). Вот еще (немного старо?):

• http://www.cis.upenn.edu/~bcpierce/courses/629/papers/Saraswat-javabug.html

А ещё в тему:

• https://www.youtube.com/watch?v=SWTWkYbcWU0 Особенно мне понравилась иерархия систем типов (на 33-й минуте)

(на видео была бурная реакция Stephen Kell http://www.cl.cam.ac.uk/~srk31/blog/2014/10/07/ , отшитая в блоге http://psnively.github.io/blog/2014/10/14/Curry-Howard-the-Ontological-Ultimate/ ).

Еще заметил, что в статье не упомянуто, что полностью реализовать типобезопасность на этапе компиляции невозможно, в общем случае нужна поддержка в рантайме. (Вот только не помню, где об этом читал, в англовики почему-то нет источника) РоманСузи 18:57, 26 ноября 2014 (UTC)

• У Larry Paulson есть, сошлюсь. И благодарю за высокую оценку. Arachnelis 10:52, 28 ноября 2014 (UTC)
• а шаблон "не переведено" ботами сам удалится или надо обходить ссылки сюда вручную? Arachnelis 08:27, 30 ноября 2014 (UTC)
  • Точно не знаю. Полагаю, что нужно обходить. РоманСузи 09:05, 30 ноября 2014 (UTC)
  • Боты исправляют некоторые шаблоны. См. например MLton. РоманСузи 13:11, 30 ноября 2014 (UTC)
• С вопросом «невозможности» надо разобраться досконально, ибо надо смотреть, что КОНКРЕТНО ещё в рантайме нужно кроме управления памятью, насколько стары источники, не появилось ли уже после них опровергающих решений. Просто способы статически обходиться с управлением динамической памятью уже существуют. По крайней мере, Cyclone и Mercury заявляют, что GC им в рантайме не нужен. MLKit вроде как должен был без него обходиться, но 4-я версия комбинирует GC с регионами. SPARK просто выбрасывает динамическую память. Соответственно, некоторый язык может и исключения не реализовывать. То есть нужно некое формальное доказательство того, что без рантайма с Тьюринг-полнотой вообще принципиально никак, а не что «без него никак данному конкретному языку». Arachnelis 10:15, 23 декабря 2014 (UTC)
  • По крайней мере, в одну сторону: Для любого Тьюринг-полного языка множество программ с ошибками типа (в рантайме) алгоритмически неразрешимо. То есть, компиляторы должны отбрасывать целые классы программ без ошибок. РоманСузи 11:02, 23 декабря 2014 (UTC)
    • Спасибо, многообещающая книжка, я там почитаю, но непосредственно по ссылке это не то. Здесь говорится, что проверка типов избыточна (консервативна), то есть "на всякий случай" отвергает даже программы, которые не привели бы к ошибке в рантайме. Аналогичная избыточность уже описана - в отношении безопасности памяти. Но и это, конечно, тоже можно приписать. Arachnelis 06:34, 26 декабря 2014 (UTC)

Проработал источники и выяснил, что в английской была написана полнейшая демагогия и отсебятина. «Типобезопасность» нигде не рассматривается как ГРАДАЦИЯ — она рассматривается как БУЛЕВА величина: или типобезопасно (то есть контроль типов в рантайме становится не нужен), или нет. Уже четыре очень разных источника это утверждают, ещё по Аде проработать можно — наверняка пятый выйдет. То, что у них было написано про динамическую типизацию и «memory type safety» было написано без единого АИ. Я не видел ни одного источника, который бы называл динамическую систему типов «safe» или «sound» (не «strong»). Райт и Феллайзен ни коим боком не смягчили трактовку безопасности до динамических языков. Они вообще не занимались формулировкой «определения безопасной системы типов» — они исследуют возможность более простого и универсального доказательства надёжности для системы типов Хиндли-Милнера, чем предшествующие педантичные и частные. Аннотация к работе: «We present a new approach to proving type soundness for Hindley/Milner polymorphic type systems». Если кто-то хочет заявить, что их доказательство применимо и к другим системам типов, то это ещё само по себе требует доказательства. Далее, приведения нотаций «сохраняемости» и «продолжаемости» явным образом я там не нашёл. Но даже если просто взять фразу, которая была в английской статье: «прошедшая проверку типов программа никогда не „застрянет“, то есть не войдёт в неопределённое состояние, при котором никакие дальнейшие операции не возможны» — то только искуссный демагог сумеет сделать из этого вывод, что «это является свойством динамической семантики» и тем более, что «под это определение попадает множество языков». Здесь же русским по белому написано: « прошедшая проверку типов». Уже прошедшая, и не абы где, а уже в рамках системы типов с доказанной надёжностью. Короче, я переписываю русскую статью под ноль, а там глядишь и с английской поспорить наглости хватит. Arachnelis 09:13, 20 января 2015 (UTC)

• Ок. Но тем не менее какая-то связь должна быть между type safety и memory safety. Например, [1]. Значит, откуда-то это идёт. Чисто интуитивно, я так понимал type safety в двух ипостасях: безопасность работы с «железом» и безопасность формализации алгоритма (термины мои), то есть, программа она как бы меж двух огней. Программер может неверно кодировать «алгоритм», но ещё хуже, когда это затрагивает нижележащий уровень (если в языке это допустимо, уровень абстракции настолько дырявый). РоманСузи 10:18, 20 января 2015 (UTC)

• Если всё type safe, то, как следствие, всё и memory safe. А на мейнстрим ссылки нам не помогут - там только демагогия. Arachnelis 15:33, 20 января 2015 (UTC)

• А знаете, я, наверное, не совсем прав. Если сильно типизированный язык поддерживает массивы с произвольным доступом (Pascal, SML), то проверка выхода индекса за границы может производиться только в рантайме. У Ахо-Сети-Ульмана это сказано, но я как-то проигнорировал. Arachnelis 18:24, 21 января 2015 (UTC)

Программы, прошедшие проверку типов, не могут «сбиться с пути истинного»

В статью вставлена фраза Робина Милнера, процитированная в заголовке данной темы. Мне кажется, тут очень-очень сильно не хватает контекста или пояснений. Ведь в текущем виде фраза выглядит как полный абсурд, поскольку сильное обобщающее утверждение (не могут «сбиться с пути истинного») делается на слишком слабом для этого основании (прошедшие проверку типов). Любой специалист согласиться, что типобезопасность вовсе не гарантирует то, что программа не может «сбиться с пути истинного». У меня нет первоисточника, поэтому прошу того, у кого он есть, скорректировать фразу так, чтобы она не выглядела столь глупо. Если же этого добиться невозможно, то и смысла в приведении данной цитаты нет, её следует удалить. Евгений Мирошниченко 15:15, 4 февраля 2017 (UTC)

• Добавил ссылку на публикацию. Bsivko (обс.) 15:28, 4 февраля 2017 (UTC)
• Слоган упоминается например тут:

Robin Milner famously said “well typed programs don’t go wrong” [Mil78]. To “go wrong” means to exhibit undefined behavior. For example, programs written in strongly statically typed programming languages cannot crash, write to random memory locations, or read past the end of a buffer. In the study of programming languages it is generally accepted that these are undesirable behaviors.

— https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.pdf

Bsivko (обс.) 15:37, 4 февраля 2017 (UTC)

• Что ж, я просмотрел статью, но пока не вижу, как можно скорректировать цитату так, чтобы она не выглядела глупой. Зачем вообще она нужна? Согласно ВП:Цитирование «Если нет уверенности, что именно эта цитата необходима и именно в этом месте текста, то лучше от цитирования отказаться». Евгений Мирошниченко 15:40, 4 февраля 2017 (UTC)

  В данном случае это слоган, и к нему не следует придираться формально. Дополнительно кавычки «с пути истинного» говорят об этом. Bsivko (обс.) 15:46, 4 февраля 2017 (UTC)

  По-моему, здесь проблема в подаче. «Робин Милнер определил рамки типобезопасности» - явно разговор идёт не о рамках. Помимо этого, доп источники говорят о «famously said», что намного лучше отражает цитату. Bsivko (обс.) 15:51, 4 февраля 2017 (UTC)

  Википедия не знает какого-то специального понятия «слоган», нет? Если это цитата, это цитата. Второе, в статье Милнера это просто кусок фразы из абстракта статьи, «слоганом» его в источниках не называют. Зачем эта фраза нужна в статье, непонятно, поскольку сама по себе фраза не только ничего полезного не утверждает, но и утверждает нечто вредное. А по правилам, «Если нет уверенности, что именно эта цитата необходима и именно в этом месте текста, то лучше от цитирования отказаться». Евгений Мирошниченко 17:28, 4 февраля 2017 (UTC)

  Выше ссылка на диссертацию в CS, которая начинается с этой цитаты. Оченьвидно, что цитата значима. Другой вопрос в чём она значима и как описана в контексте. Скорее всего в статью она попала из англовики, но по пути смысл и форма были обезображены. Bsivko (обс.) 21:21, 4 февраля 2017 (UTC)