Здравствуйте, Pavel Dvorkin, Вы писали:
PD>Может, тебе основы организации компьютера почитать ? Чтобы понять, что независимо от языка, при выполнении программы дело закончится некими действиями с блоками памяти ? По крайней мере до тех пор, пока вместо ОП не появятся аппаратно реализованные абстракции твоего любимого языка.
А зачем мне про это читать? Это ты всё время путаешь уровни абстракции.
Вот ты говоришь:

дело здесь не в будущем, а в существе — мы все же в программе имеем намного больше переменных, чем констант, пусть и временно живущих.

Ты здесь под программой что имеешь в виду? Исходную программу, или её некоторое воплощение в код реальной машины?

Большинство программистов таки понимают первое. В таком контексте, переменная (storage) — это чисто математическая абстракция, которая применяется при описании семантики языков программирования. Не всех, разумеется, а только некоторого подмножества императивных.
Опять же, намекну, что даже императивному языку не обязательно оперировать переменными. К примеру, HPGL без них прекрасно обходится, являясь, в сущности, взрослым развитием языка LOGO.

Но дальше ты говоришь про "выполнение программы". Тут как бы ты перепрыгиваешь на уровень ниже — там от программы почти ничего не остаётся. Да, там есть что-то вроде "блоков памяти" (ну, то есть даже внутри "аппаратной машины" всё еще есть разные уровни абстракции; на более высоких есть только регистры ЦПУ, память и порты, а на более низких видны все детали буферов, защёлок и прочих потрохов различных устройств). Но никаких переменных к этому моменту уже не остаётся.

И нас как раз очень-очень мало* интересует вопрос о том, какой процент блоков памяти перезаписывается при выполнении программы.

Иммутабельность переменных не имеет к этому никакого отношения. Я в очередной раз попробую открыть тебе америку: даже самая императивная программа на языке вроде C++ при компиляции на время переводится в SSA форму. Это как раз та форма, где каждая переменная получает значение ровно один раз, становясь, таким образом, иммутабельной. И уже из этой формы оптимизатор получает необходимый набор низкоуровневых манипуляций с регистрами и памятью.

(*) Точнее, нас интересует этот и прочие вопросы. Но он интересует нас в отрыве от исходной программы. Мы хотим, чтобы исходная программа была
а) как можно понятнее (чтобы меньше был шанс сделать в ней ошибку, и больше был шанс ошибку найти)
б) как можно короче (чтобы меньше было места сделать ошибку)
в) как можно менее навязчивой в описании того, какие именно операции мы хотим от железки — чтобы развязать руки оптимизатору.

Вот пункт в как раз и есть про оптимизацию. Начинающим программистам кажется, что самый дружественный к оптимизации язык — это такой, на котором можно делать ассемблерные вставки. Неа. Самый дружественный — это такой, в котором нельзя делать ассемблерные вставки.

Здравствуйте, WolfHound, Вы писали:

WH>В случае применения зависимых типов программа не скомпилируется пока не напишешь так что переполнений гарантировано не будет и вирус снова не у дел.
WH>Причем без единой проверки во время работы программы. Все компилятор поймает.

Все эти возможности доступны и сейчас в том же С++, однако не особо народ юзает. Не подскажешь, почему?

Здравствуйте, Sinclair, Вы писали:

S>Здравствуйте, Pavel Dvorkin, Вы писали:
PD>>Может, тебе основы организации компьютера почитать ? Чтобы понять, что независимо от языка, при выполнении программы дело закончится некими действиями с блоками памяти ? По крайней мере до тех пор, пока вместо ОП не появятся аппаратно реализованные абстракции твоего любимого языка.
S>А зачем мне про это читать? Это ты всё время путаешь уровни абстракции.
S>Вот ты говоришь:
S>

дело здесь не в будущем, а в существе — мы все же в программе имеем намного больше переменных, чем констант, пусть и временно живущих.

S>Ты здесь под программой что имеешь в виду? Исходную программу, или её некоторое воплощение в код реальной машины?

Разумеется, второе. На языке могут быть явно описаны переменные или константы. На языке (вполне традиционном) они могут быть заданы неявно или сгенерированы компилятором

int i = 2*2;

и в рабочем коде нет 2, а есть 4, ибо это сделано на этапе компиляции. Хотя я 4 не заводил.

В языке может вообще не быть переменных. Он может быть некоего описательного типа, при этом переменные генерируются компилятором/средой выполнения. Но они все равно есть.


S>Большинство программистов таки понимают первое. В таком контексте, переменная (storage) — это чисто математическая абстракция, которая применяется при описании семантики языков программирования. Не всех, разумеется, а только некоторого подмножества императивных.

Как большинство понимает — это мне сейчас не так важно. Напомню, речь шла о константных и неконстантных объектах. Сгенерировал ли их компилятор по некоему явному описанию или же завел их так, что я их и не вижу в своем коде — они все равно либо константны, либо нет. Проще говоря, эти блоки памяти будут изменяться или нет. Если будут — их нельзя в R/O память. Если не будут — можно. Все.

S>Но дальше ты говоришь про "выполнение программы". Тут как бы ты перепрыгиваешь на уровень ниже — там от программы почти ничего не остаётся. Да, там есть что-то вроде "блоков памяти" (ну, то есть даже внутри "аппаратной машины" всё еще есть разные уровни абстракции; на более высоких есть только регистры ЦПУ, память и порты, а на более низких видны все детали буферов, защёлок и прочих потрохов различных устройств). Но никаких переменных к этому моменту уже не остаётся.

Не занимайся софистикой. Регистры могу добавить, согласен, переменные могут быть и на регистрах, а что касается потрохов — они ниже программирования и меня не интересуют. Равно как и сигналы шины и т.п. Я не схемотехник.


S>Вот пункт в как раз и есть про оптимизацию. Начинающим программистам кажется, что самый дружественный к оптимизации язык — это такой, на котором можно делать ассемблерные вставки. Неа. Самый дружественный — это такой, в котором нельзя делать ассемблерные вставки.

Здравствуйте, Sinclair, Вы писали:

S>Здравствуйте, swined, Вы писали:
S>>ты же сам сказал, что верификацией должен заниматься компилятор. компилятор работает не на твоей машине и слитый из интернетов бинарь может содержать все, что угодно.
S>Нет, это ты путаешь. Верификатор — совершенно отдельная штука. Его нужно делать как можно более компактным, потому что его верификация выполняется вручную. Вручную верифицировать огромный компилятор ты запаришься.

кстати да, каким бы компактным не был верификатор, в нем могут быть ошибки. хардварная защита как-то понадежней будет.

S>>бтв, как ты смотришь на необходимость длительной и ресурсоемкой верификации перед каждой установкой каждой программы?
S>Верификация делается за O(N), где N — размер программы

ссылочку на способы такой верификации не дашь? мне все это пока представляется как статический анализ, который нифига не выполним за O(N). причем, для native-кода он будет еще медленнее из-за отсутсвия высокоуровневых конструкций типа foreach, вместо которого пришлось бы разбирать обычный цикл и проверять его на выход за границы.

Здравствуйте, Sinclair, Вы писали:

S>Здравствуйте, Pavel Dvorkin, Вы писали:

PD>>Ты уже давно заметил, что для меня все непонятно . Я уже давно решил, что на эти высказывания не стоит обращать серьезного внимания
S>Это твоё право. Но очень зря. Потому что обращая внимание на непонятные тебе вещи, ты бы смог сделать свои программы лучше.

Вряд ли. Во всяком случае следуя твоим советам — с точностью до наоборот

>Помнишь, мы обсуждали длины строк? Статистически 99% строк в природе оборудованы длиной от момента своего рождения.

У тебя. А у меня нет.

>Игнорирование этого факта приводит к чудовищно неэффективным алгоритмам на строках.

Напомню тебе, коли уж так, что я как раз и говорил, что тем строкам, которые оборудованы и т.д от рождения и не изменятся, им можно при рождении и поставить. А тем. что не оборудованы, не надо. Прицепление же этой длины ко всем строкам и перевычисление ее каждый раз для тех, кому это не надо, именно к неэффективным алгоритмам и ведет.


S>При этом аргумент в пользу игнорирования ровно один: "а вдруг там не будет длины".

Нет, аргумент другой — а нужна ли там длина ? От ответа все и зависит.

S>Я имею в виду, что я согласен на инфраструктуру, которая ловит 99% ошибок. Это в 100 раз сократит мне время отладки.

Каких ошибок ? IndexOutOfRange — для меня мелочи. AccessViolation — тоже. А вот FloatOverflow отловишь ? ZeroDivide ? И т.д.

Ты действительно отловишь даже не 99, а 100% ошибок, но только для 1% возможных ошибок.

PD>>Поэтому мне и не кажется серьезным такая забота об этих мелочах. Серьезные вещи вы все равно не улучшите, так как неформализуемо это (см. пример с плюсом-минусом, а это самый примитивный из тех, что я могу придумать)
S>Придумывание контрпримеров — это хорошо. Это правильно.

Поздравляю тебя с тем, что ты это понял


>Но начиная примерно с 90го года рулят алгоритмы, которые затачиваются не на максимальное быстродействие в самом хреновом случае, а на максимальное среднее быстродействие с учётом реальной статистики.

А при чем тут самый плохой случай ? Где я говорил, что оптимизирую именно под самый плохой ? Опять передергиваешь.



PD>>Я никак не считал, но приведи мне эти самые иммутабельные типы в нынешней библиотеке. String, DateTime... сколько еще покажешь общеупотребимых ?
S>Uri. Regex. Дело не в этом — ты же считаешь, что это связано с какими-то "ограничениями". Хотелось бы аргументов на эту тему.

А еще , пожалуйста , можешь ? Ну хоть 10% от общего числа классов иммутабельно ? Вот тебе и ответ насчет ограничений — они в том. что таких классов исчезающе мало. Константные типы редки по смыслу самому. А вот константные экземпляры — бога ради, любого типа. Создали однажды и менять не нужно — вот он и константный.

PD>>Нет. Я, кстати, отнюдь не С-шник по первому языку. И мне язык в данном случае безразличен, правда, ограничусь императивными.
S> Да не безразличен тебе язык. Ты мыслишь императивными

Совершенно верно. По причине императивности устройства, которое все это исполнять будет (процессор+память). Вот когда процессор будет функциональным, а память реализует физически абстракции некоего языка. тогда я изменю свой подход. А пока за всеми языками я вижу то, во что они превращаются при исполнении. И чем меньше там лишнего, тем лучше.

>причём построенными по одной и той же модели с минимальными синтаксическими различиями.

Тоже верно. По причине минимальных синтаксических различий (точнее, их отсутствия) у того, кто все это исполнять будет — см. чуть выше.

Здравствуйте, Sinclair, Вы писали:

S>Я имею в виду, что я согласен на инфраструктуру, которая ловит 99% ошибок. Это в 100 раз сократит мне время отладки.

Честно говоря, меня только 3 вида исключений всерьез интересует. Правда, они никогда исключениями в прямом смысле не бывают. Вот они

InvalidImpementationException. Алгоритм правильный и хороший, но реализовал я его неправильно и из-за этого ничего не работает
InvalidAlgorithmException. Алгоритм мне казался правильным, но увы, в нем не все верно или вообще неверно, и из-за этого ничего не работает
TooSlowCodeException Алгоритм правильный, работает верно, но очень уж медленно, а это для меня все равно , что не работает вообще — все равно заказчик его не примет



Вот на это я 99% времени и трачу. А на выход индекса за пределы массива я трачу 0.1%. Пишите код так, чтобы не выходил, вот и все.

Здравствуйте, thesz, Вы писали:

T>Но они могут быть и достаточно большими. Например, для одной моей программы требуется -fcontext-stack=100, то есть, она совершает не менее 100 шагов упрощения типов вычислениями над ними с семействами типов (type families). Проверка типов занимает заметное время порядка 30 секунд.
Я можно подробнее?
Нет ли там выкрутасов аля шаблонная метамагия в С++?
И не будет ли это все сильно проще при наличии зависимых типов?

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Тебе же тут уже объяснили — не работайте под админом. Кстати, как ты собираешься устроить эту самую эскалацию для процесса броузера, если он (под Вистой) запущен хоть и от админа, но без админских прав ? (т.е с юзеровскими правами) Это тоже очень интересно бы знать
Через переполнение буфера например.
Что думаешь в WinAPI ни одного нет?
И если ты так думаешь то на каком основании?

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>Вряд ли. Иначе зачем ерунду пишешь ?
Ерундой она кажется только тем кто за деревьями не видит леса.

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>В языке может вообще не быть переменных. Он может быть некоего описательного типа, при этом переменные генерируются компилятором/средой выполнения. Но они все равно есть.
Еще раз: при этом никакие переменные не генерируются. Ну, то есть, в частных случаях — да. Например, в дотнете есть понятие "locals", т.е. локальные переменные. И они таки да — генерируются компилятором (причём не обязательно каждой переменной исходного кода соответствует отдельный слот в таблице locals, и наоборот).
Но, к примеру, в x86 ассемблере никаких "переменных" нет. Есть регистры и стек; компилятор генерирует исключительно обращения к ним.

PD>Как большинство понимает — это мне сейчас не так важно. Напомню, речь шла о константных и неконстантных объектах. Сгенерировал ли их компилятор по некоему явному описанию или же завел их так, что я их и не вижу в своем коде — они все равно либо константны, либо нет. Проще говоря, эти блоки памяти будут изменяться или нет. Если будут — их нельзя в R/O память. Если не будут — можно. Все.
Это всё так же далеко от правильного понимания. Ты опять путаешь "константы" и "иммутабельные объекты".
Поясняю: даже если объект иммутабельный, в R/O память его положить нельзя. Ну, разве что ты собрался выделять по 4к на каждый экземпляр. Потому, что в отличие от константы, значение immutable объекта может не быть доступно на момент старта программы. И, в отличие от константы, иммутабельный объект не существует неограниченно долго.
С точки зрения аппаратуры, место, занятое иммутабельным объектом, всё же выступает в роли lvalue — в него сначала присваивают некоторое значение, потом сколько-то раз им пользуются, а потом повторно используют это же место под другие объекты (потому, что аппаратуры с неограниченным объемом storage еще не придумали).
Использование аппаратной защиты для обеспечения иммутабельности на реальной аппаратуре просадит производительность. А, главное, не даст никакого выигрыша даже на "идеальной" аппаратуре, где запрет записи делается бесплатно с гранулярностью до байта.

PD>Не занимайся софистикой. Регистры могу добавить, согласен, переменные могут быть и на регистрах, а что касается потрохов — они ниже программирования и меня не интересуют. Равно как и сигналы шины и т.п. Я не схемотехник.
Я уже понял, что ты воспринимаешь ровно один уровень абстракции. Ни подняться выше, ни спуститься ниже ты не хочешь. Ок, это твой свободный выбор, добровольное самоограничение.

Здравствуйте, swined, Вы писали:
S>кстати да, каким бы компактным не был верификатор, в нем могут быть ошибки. хардварная защита как-то понадежней будет.
Ты полагаешь, что хардварная защита разрабатывается сверхлюдьми?
Не волнуйся. В случае, если в верификаторе ошибка (а его текст очень невелик)
S>ссылочку на способы такой верификации не дашь? мне все это пока представляется как статический анализ, который нифига не выполним за O(N).
Гм. Почитай, что ли, как работает дотнетовый верификатор. В джаве, афаир, тоже есть аналогичный верификатор. Там всё очень просто — накладываются некоторые ограничения на программы, и из "проблемы останова" мгновенно получаем линейную задачу.
S> причем, для native-кода он будет еще медленнее из-за отсутсвия высокоуровневых конструкций типа foreach, вместо которого пришлось бы разбирать обычный цикл и проверять его на выход за границы.
Гм. Во-первых, для native-кода верификатор построить нельзя. Иначе бы он давно уже существовал.
Во-вторых, "высокоуровневые конструкции" к верификатору никакого отношения не имеют. Я, наверное, тебя удивлю, но инструкции foreach в MSIL нету. Сплошные conditional jump-ы.

Речь идет вот о чём: верификатор проверяет исключительно типобезопасность. То есть после проверки мы знаем, что никакая инструкция программы не станет обращаться с объектом типа A как с объектом несовместимого с ним типа B.
Подчеркну: это то, что уже есть.
То, чего нету — это богатой системы типов, которая влияет на понятие "совместимости" во фразе выше.
Например, более мощная система типов, чем в CLR, позволила бы устранить само понятие NullReferenceException, благодаря тому, что NotNullable типы отделялись бы от Nullable. При этом сам верификатор изменять бы было совершенно ненужно: тот же самый код за те же самые O(N) обнаруживал бы все нарушения. В случае, если ты захакал компилятор, конечно — потому что в противном случае тебе бы компилятор с самого начала сказал "извини, чувак, но длину от возможно-null строки я тебе вычислять не дам".

Более мощная система типов позволила бы за те же деньги отлавливать ошибки типа "незаескейпленная строка". Или "хранение секретных данных в незашифрованном виде". Или "обработка занимает больше тактов, чем можно".

И это только то, что я понимаю своим невооруженным мозгом. Более продвинутые чуваки утверждают, что типами можно описать еще более сложные штуки — типа отсутствия race condition и прочие пряники.

Да, конечно, это всё никак не поможет Павлу Дворкину. Потому что у него не так страшно получить противоречивую спецификацию (что как раз и может обнаружить верификатор), как получить некорректную непротиворечивую (потому что это как раз никакой верификатор не заметит).

Здравствуйте, Pavel Dvorkin, Вы писали:

PD>InvalidImpementationException. Алгоритм правильный и хороший, но реализовал я его неправильно и из-за этого ничего не работает
Ну, во многих случаях InvalidImplementation сводится к InconsistentImplementation. Это уже математически обнаружимая ошибка. Например, вычисление среднего не от всех переданных аргументов.

PD>InvalidAlgorithmException. Алгоритм мне казался правильным, но увы, в нем не все верно или вообще неверно, и из-за этого ничего не работает
Это да. Если вместо алгоритма вычисления среднего арифметического ты вычислил среднее геометрическое — никакая магия не спасёт.
PD>TooSlowCodeException Алгоритм правильный, работает верно, но очень уж медленно, а это для меня все равно , что не работает вообще — все равно заказчик его не примет
А вот это — тоже вполне себе разрешимая задачка. Если среда умеет выводить и проверять контракты на вычислительную сложность, то ты можешь очень быстро увидеть, где именно боттлнек, еще до запуска профайлера.
PD>Вот на это я 99% времени и трачу. А на выход индекса за пределы массива я трачу 0.1%. Пишите код так, чтобы не выходил, вот и все.

Здравствуйте, vdimas, Вы писали:

V>Не ожидал от тебя такого заявления.
V>Ты точно знаешь, о чем говоришь?
Да. А ты точно не знаешь что такое зависимые типы ибо в С++ их нет.
В С++ типы не могут зависит от данных полученных во время работы программы.

V>Не важно чем, если есть ср-ва прочитать/записать хотя бы байт из/в произвольного участка памяти, то вся безопасность и доказуемость сразу улетучивается.
ХА! Эти средства использует кодогенератор генерирующий код по верифицированной модели.

Здравствуйте, vdimas, Вы писали:

V>Блин, тебе хочется хлеба и зрелищ? Ну давай покажи как можно в ОбЩЕМ случае. Заодно список языков с примерами.
Сначала пойми что такое зависимые типы. После чего вопросы у тебя отпадут сами собой.
А заниматься твоим образованием у меня нет никакого желания.

Здравствуйте, vdimas, Вы писали:

V>Все эти возможности доступны и сейчас в том же С++, однако не особо народ юзает. Не подскажешь, почему?
Ты хочешь сказать что для любой программы на С++ можно доказать что она нигде не проедется по памяти?

Здравствуйте, swined, Вы писали:

S>кстати да, каким бы компактным не был верификатор, в нем могут быть ошибки. хардварная защита как-то понадежней будет.
А в хардварной защите ошибок быть не может?
Тем более что верификатор сам себя проверить может что снижает вероятность ошибки до нуля.
Можно даже написать 2 или более верификаторов каждый из которых будет проверять как себя так и всех остальных.
В этом случае ошибка вообще хрен проскочит.

S>ссылочку на способы такой верификации не дашь? мне все это пока представляется как статический анализ, который нифига не выполним за O(N).
У нас в бинарнике что?
Типизированный код.
И верификация сводится к банальной проверки того что все типы совпадают.
А это O(N).

S>причем, для native-кода он будет еще медленнее из-за отсутсвия высокоуровневых конструкций типа foreach, вместо которого пришлось бы разбирать обычный цикл и проверять его на выход за границы.
Так и не надо заниматься фигней и верифицировать нативный код.

Здравствуйте, Sinclair, Вы писали:

S>Ты полагаешь, что хардварная защита разрабатывается сверхлюдьми?

я полагаю, что она разрабатывается достаточно давно, чтобы наступить на все возможные грабли и исправить практически все возможные ошибки.

S>Не волнуйся. В случае, если в верификаторе ошибка (а его текст очень невелик)

так что же будет в этом случае?

S>Гм. Почитай, что ли, как работает дотнетовый верификатор. В джаве, афаир, тоже есть аналогичный верификатор. Там всё очень просто — накладываются некоторые ограничения на программы, и из "проблемы останова" мгновенно получаем линейную задачу.

дык оно же поймает ничтожно малую часть возможных проблем.

S>Гм. Во-первых, для native-кода верификатор построить нельзя. Иначе бы он давно уже существовал.

так что же тогда предлагается верифицировать? как я смогу использовать бинарь слитый из интернетов с непонятных варез-сайтов? или придется городить ms signed software, drm и прочую хрень созданную для того, чтобы у меня работало только три программы, две из которых — пасьянс?

S>Во-вторых, "высокоуровневые конструкции" к верификатору никакого отношения не имеют. Я, наверное, тебя удивлю, но инструкции foreach в MSIL нету. Сплошные conditional jump-ы.

однако перед генерацией IL'а они есть, чем сильно помогают компилятору.

S>Речь идет вот о чём: верификатор проверяет исключительно типобезопасность. То есть после проверки мы знаем, что никакая инструкция программы не станет обращаться с объектом типа A как с объектом несовместимого с ним типа B.
S>Подчеркну: это то, что уже есть.

а толку? как ты будешь проверять те же массивы на границы?

S>То, чего нету — это богатой системы типов, которая влияет на понятие "совместимости" во фразе выше.
S>Например, более мощная система типов, чем в CLR, позволила бы устранить само понятие NullReferenceException, благодаря тому, что NotNullable типы отделялись бы от Nullable. При этом сам верификатор изменять бы было совершенно ненужно: тот же самый код за те же самые O(N) обнаруживал бы все нарушения. В случае, если ты захакал компилятор, конечно — потому что в противном случае тебе бы компилятор с самого начала сказал "извини, чувак, но длину от возможно-null строки я тебе вычислять не дам".

отделение nullable от not nullable только сократит количество ошибок, но не избавит от них полностью. что мне мешает иметь nullable string, который абсолютно легален в логике программы, и иногда считать его длину?

S>Более мощная система типов позволила бы за те же деньги отлавливать ошибки типа "незаескейпленная строка". Или "хранение секретных данных в незашифрованном виде". Или "обработка занимает больше тактов, чем можно".
S>И это только то, что я понимаю своим невооруженным мозгом. Более продвинутые чуваки утверждают, что типами можно описать еще более сложные штуки — типа отсутствия race condition и прочие пряники.

а где бы почитать об этом?

Здравствуйте, WolfHound, Вы писали:

WH>Тем более что верификатор сам себя проверить может что снижает вероятность ошибки до нуля.

верификатор не проверит логику.

WH>У нас в бинарнике что?
WH>Типизированный код.

типизированный? в бинарнике? там же просто куча процессорных инструкций перекладывающих байты

WH>Так и не надо заниматься фигней и верифицировать нативный код.

а что еще с ним делать, если нет другого?

Здравствуйте, swined, Вы писали:

S>я полагаю, что она разрабатывается достаточно давно, чтобы наступить на все возможные грабли и исправить практически все возможные ошибки.
Тут пожалуй нужно спросить у thesz но мне почему то кажется что на практике дело без программных верификаторов этих проверок не обходится...

S>дык оно же поймает ничтожно малую часть возможных проблем.
В случае с системой типов .NET да. А вот в случае с более умной системой типов поймает куда больше.
Давать эту ссылку мне уже надоело http://en.wikipedia.org/wiki/Dependent_type

S>так что же тогда предлагается верифицировать? как я смогу использовать бинарь слитый из интернетов с непонятных варез-сайтов?
Нативный? Никак. Те вообще никак.

S>или придется городить ms signed software, drm и прочую хрень созданную для того, чтобы у меня работало только три программы, две из которых — пасьянс?
Нет. Если все бинари будут представлять из себя верефицируемый промежуточный код то нет.
Достаточно чтобы бинарь верификацию прошол.

S>>Во-вторых, "высокоуровневые конструкции" к верификатору никакого отношения не имеют. Я, наверное, тебя удивлю, но инструкции foreach в MSIL нету. Сплошные conditional jump-ы.
S>однако перед генерацией IL'а они есть, чем сильно помогают компилятору.
Это ты сказал от полного незнания того как это все работает.

S>а толку? как ты будешь проверять те же массивы на границы?
Зависимые типы.

S>отделение nullable от not nullable только сократит количество ошибок, но не избавит от них полностью. что мне мешает иметь nullable string, который абсолютно легален в логике программы, и иногда считать его длину?
Отсутствие nullable string.
Вместо nullable будет что-то типа

variant Option[T]
{
| Some { value : T }
| None
}

И соответственно будет Option[String]. И длину у этого дела посчитать невозможно пока не достанешь строку из данного варианта.

S>а где бы почитать об этом?
Давать эту ссылку мне уже надоело http://en.wikipedia.org/wiki/Dependent_type

Здравствуйте, swined, Вы писали:

WH>>Тем более что верификатор сам себя проверить может что снижает вероятность ошибки до нуля.
S>верификатор не проверит логику.
Логика проверена системой типов.

S>типизированный? в бинарнике? там же просто куча процессорных инструкций перекладывающих байты
Ты на бинарники программ под .NET или жабу посмотри да.

WH>>Так и не надо заниматься фигней и верифицировать нативный код.
S>а что еще с ним делать, если нет другого?
Друго нет только в твоем воображении.