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

Хотел написать большой развернутый ответ но понял что бесполезно.
Ибо объяснять что либо человеку который не может выйти за приделы одного уровня абстракции совершенно бесполезно.
На этом разговор с тобой закончил.

Здравствуйте, swined, Вы писали:
S>так что же будет в этом случае?
Мы просто выпустим к нему апдейт

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

S>однако перед генерацией IL'а они есть, чем сильно помогают компилятору.
А причём тут компилятор? Он верификацией не занимается. Его работа — всего лишь породить корректный IL.

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

S>отделение nullable от not nullable только сократит количество ошибок, но не избавит от них полностью.
Это полностью избавит от ошибок NullReferenceException.
S>что мне мешает иметь nullable string, который абсолютно легален в логике программы, и иногда считать его длину?
То, что null стринг не имеет длины по определению. В хорошем языке ты не сможешь написать просто int HalfLength(string a) {return a.Length}
Ты будешь обязан либо писать

int HalfLength(string a)
{
    if (a != null)
    {
        return a.length;
    }
}

(и компилятор трахнет тебя за not all paths return a value), либо писать

int HalfLength([NotNull] string a)
{
    return a.length;
}

И тогда компилятор будет трахать того, кто пытается вызывать HalfLength на нуллабл-строке.
S>а где бы почитать об этом?
Ну, в этом форуме много про это пишут.

Здравствуйте, swined, Вы писали:
S>типизированный? в бинарнике? там же просто куча процессорных инструкций перекладывающих байты
Поэтому у бинарников, где "просто куча процессорных инструкций перекладывающих байты" и нет будущего.
S>а что еще с ним делать, если нет другого?
Придумывать другой. В сингуларити, например, нет никакого нативного кода, кроме 1 килобайта в недрах ядра. Для неё "слить из интернета" можно только промежуточное представление.

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

Есть.

WH>И не будет ли это все сильно проще при наличии зависимых типов?

Шаблоны и есть зависимые типы.

Поэтому заметно проще не будет.

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

S>Пример иллюстрировал тот факт, что ты привык применять определённые средства, совершенно неудобные для твоей задачи. Но ты привык это делать настолько хорошо, что теперь тебе сложно воспринять более простые вещи. Верификация кода не имеет к твоим проблемам никакого отношения. Да, наверное, MSIL не лучший язык для записи твоих задач. Но и ассемблер — тоже. По-хорошему, это должен быть DSL, который очень компактно и понятно отражает суть алгоритма. А упаковка алгоритма в битхакинг — дело компилятора.

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

EYE_CAR
  ..
  .*.

EYE_2x3
  .*.
  .*.

Соответственно по этому исходники генерируется функция

  int AnalyzeEye(const Bitgoban* eye_mask, Bitgoban* critical_points)
  {
  ...
  }

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

По поводу использования DSL для конкретной задачи написания шахматного движка... Как по мне, для этой задачи лучше всего подходит C. И так считают разработчики многих сильнейших движков. Разработка специального DSL для записи алгоритмов такого рода будет достаточно трудоемкой задачей. К тому же производительность достаточно важна, так что полностью абстрагироваться от низкого уровня вряд ли получится. И задача разработки такого DSL получится в чем-то даже сложнее исходной задачи. Плюс весь комплекс сопутствующих инструментов: отладка, профайлер и т. п.

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

T>Шаблоны и есть зависимые типы.
Я бы не стал называть шаблоны С++ зависимыми типами.
Ибо как ни крути, а типы в С++ не могут зависеть от значений полученных по время исполнения программы.

T>Поэтому заметно проще не будет.
А можно посмотреть на код? Если не секрет конечно. Можно по почте.

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

WH>Нативный? Никак. Те вообще никак.

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

WH>Это ты сказал от полного незнания того как это все работает.

тут считают подругому. аналогичные оптимизации делаются и для foreach чуть более очевидным образом.

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

либо компилятор заенфорсит меня написать проверку перед вызовом (он и сейчас так может), либо получается та же фигня Option[String].getLength(), кидающий NullReferenceException, когда в нем нет ненулевой строки.

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

S>Мы просто выпустим к нему апдейт

но будет поздно

S>Предлагается выкинуть понятие "бинаря, слитого с непонятных варез-сайтов". Сливать можно будет только verifyable код, очевидно.

S>А причём тут компилятор? Он верификацией не занимается. Его работа — всего лишь породить корректный IL.

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

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

WH>Логика проверена системой типов.

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

WH>Ты на бинарники программ под .NET или жабу посмотри да.

это малая часть всех запускаемых бинарников.

WH>Друго нет только в твоем воображении.

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

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

S>Поэтому у бинарников, где "просто куча процессорных инструкций перекладывающих байты" и нет будущего.

но пока у них есть настоящее и с этим ничего не сделать.

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

надеюсь, что когда эта система получит хоть какое-то распространение, под нее будет достаточно программ.

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

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

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

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

PD>>InvalidAlgorithmException. Алгоритм мне казался правильным, но увы, в нем не все верно или вообще неверно, и из-за этого ничего не работает
S>Это да. Если вместо алгоритма вычисления среднего арифметического ты вычислил среднее геометрическое — никакая магия не спасёт.

Если бы так просто было...

PD>>TooSlowCodeException Алгоритм правильный, работает верно, но очень уж медленно, а это для меня все равно , что не работает вообще — все равно заказчик его не примет
S>А вот это — тоже вполне себе разрешимая задачка. Если среда умеет выводить и проверять контракты на вычислительную сложность, то ты можешь очень быстро увидеть, где именно боттлнек, еще до запуска профайлера.

Что я слышу !!! Без профайлера, оказывается, можно. Правда, если среда умеет... А если я сам умею (я могу оценить алгоритм на выч.сложность или уж совсем никак не могу ? — тогда что ? Вроде кто-то утверждал, что надо именно только с профайлером и никак иначе

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

Здравствуйте, swined, Вы писали:
S>т.е. заменить хардварные проверки верификацией для существующего софта не удастся
Конечно.
S>и мы обсуждаем тут сферических коней?
Нет, кони уже бегут, избы вполне горят.
S>либо компилятор заенфорсит меня написать проверку перед вызовом (он и сейчас так может),
Сейчас он не может избавить тебя от проверок там, где проверять не надо.
В частности, если у тебя есть две гарантированно NonNull-string на входе, то Concat от них тоже вернёт nonNull. И проверять это уже не надо.
S> либо получается та же фигня Option[String].getLength(), кидающий NullReferenceException, когда в нем нет ненулевой строки.
Нет. Никаких exception. Вся фишка — именно в том, чтобы зависимые типы выводились сами. В результате у тебя чётко оговорены места, где Nullable string превращается в NonNullable стринг. А не минное поле, где любой вызов может внезапно бросить NRE.

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

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

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

А поподробнее можно ? Вот передаем некоей Win API не тот буфер, не того размера. Насильно передаем. Объясни, что же будет.

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

PD>Мне бы твои проблемы
Я думаю, что от моих проблем ты загнёшся.
PD>В том-то и дело, что на основании простейших примеров вы беретесь делать выводы для сложных алгоритмов. А если я неправильно реализовал потому что и сам не понимаю, как тут правильно из-за сложности алгоритма, превышающншл (допустим) мои способности ?
Какая разница, по какой причине ты реализовал "неправильно"? Если "неправильно" — это неконсистентно, то всё обнаружится статической проверкой.

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

PD>Математически обнаружимая... Да, в твоем примере это сойдет. На тебе иной пример — ядро Windows. Спроектируй его в основных чертах и попробуй потом математически обнаружить, а мы посмотрим
Ну не странно ли, что для всяческих ОС ядер таки доказывают различные свойства при помощи различных theorem prover-ов?

S>>А вот это — тоже вполне себе разрешимая задачка. Если среда умеет выводить и проверять контракты на вычислительную сложность, то ты можешь очень быстро увидеть, где именно боттлнек, еще до запуска профайлера.
PD>Что я слышу !!! Без профайлера, оказывается, можно. Правда, если среда умеет... А если я сам умею (я могу оценить алгоритм на выч.сложность или уж совсем никак не могу ? — тогда что ?
Ну, так ты, наверное, и по регистрам можешь переменные вручную распределить. Но зачем, если компилятор это делает за тебя?
PD>Вроде кто-то утверждал, что надо именно только с профайлером и никак иначе
Есть некоторые нюансы. В частности, автоматически выведенным оценкам производительности я доверяю как-то больше, чем твоим. Из-за сложности алгоритма, превышающншл (допустим) твои способности.

А в общем, из оценки сложности оценить где будет реальный боттлнек далеко не всегда возможно.

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

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

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

S>Но, к примеру, в x86 ассемблере никаких "переменных" нет. Есть регистры и стек; компилятор генерирует исключительно обращения к ним.

В школу! В первый класс!!!

// комментарии мои - DP

handle  dw      ? // это что такое  ?
infobyt db      ? // а это ?
line    db      320 dup (?) // а это массив, к твоему сведению
linesiz dw      ?
stepsiz dw      ?
palette db      768 dup (?)
parseg  dw      ?
palsiz3 dw      ?
showit  db      ?
txtsize dw      ?
vs      db      ?
        .code
        mov     ax,ds
        push    ax
        mov     ax,@data
        mov     ds,ax

Честно говоря, все от тебя ожидал, но уж такое!!! Это же значит, что ты вообще не понимаешь, как работает машинная программа. Всю работу с памятью выкинул в мусорный ящик, только стек оставил. Ну и ну!

Извини, но после этого никакие вопросы, связанные с работой на уровне ниже ЯВУ обсуждать с тобой смысла не имеет.


S>Поясняю: даже если объект иммутабельный, в R/O память его положить нельзя. Ну, разве что ты собрался выделять по 4к на каждый экземпляр.

Обоснуй. Кто мне мешает там кучу завести ? Тот факт. что объекты не изменяются, не значит, что их нельзя удалять, вести список свободных блоков и т.д хоть по схеме CRT heap, хоть по схеме .Net heap.

>Потому, что в отличие от константы, значение immutable объекта может не быть доступно на момент старта программы.

И не надо. Его туда (в R/O) должен помещать специальный конструктор или new или вместе

immutable Type a = new immutable Type(...);

> И, в отличие от константы, иммутабельный объект не существует неограниченно долго.

И что с того ? См. выше — никто не мешает его удалять. Это будет делать его delete/деструктор в C++ или GCImmutable в .Net.

S>С точки зрения аппаратуры, место, занятое иммутабельным объектом, всё же выступает в роли lvalue — в него сначала присваивают некоторое значение, потом сколько-то раз им пользуются, а потом повторно используют это же место под другие объекты (потому, что аппаратуры с неограниченным объемом storage еще не придумали).

Совершенно верно.

S>Использование аппаратной защиты для обеспечения иммутабельности на реальной аппаратуре просадит производительность.

Нет. Я уже тысячу раз объяснял — проверки записи в процессоре аппаратны и делаются всегда при записи.


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

А зачем тебе доступ с этой гранулярностью ? Никаких проблем и сейчас нет.

А хочешь, я тебе секрет открою? В С++ есть иммутабельный объект. Защищается именно механизмом страничной защиты. Догадался, о чем речь идет ?

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

Мне уровни абстракции нужны в этих рассуждениях , как корове седло. Оставь их для других случаев, там я могу их обсуждать. А здесь я одно утверждаю — что ни делайте, какие средства ни придумывайте, но пока аппаратура нынешняя. все равно вы мимо этого слоя не пройдете. Вот и все.

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

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

T>>Шаблоны и есть зависимые типы.
WH>Я бы не стал называть шаблоны С++ зависимыми типами.
WH>Ибо как ни крути, а типы в С++ не могут зависеть от значений полученных по время исполнения программы.

Это зависит.

В Cayenne, Agda и тп нет оператора casetype. Поэтому ты не можешь типы в Cayenne, Agda и тп не могут зависеть от значений времени выполнения.

А вот связать значения из типов со значениями времени выполнения путём доказательств возможно. И в C++ тоже (хотя и не очень уверен).

T>>Поэтому заметно проще не будет.
WH>А можно посмотреть на код? Если не секрет конечно. Можно по почте.

Пожалуй, показать не смогу.

Части я тут выкладывал (чуть выше было), это всё, что я могу показать.

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

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

WH>Хотел написать большой развернутый ответ но понял что бесполезно.
WH>Ибо объяснять что либо человеку который не может выйти за приделы одного уровня абстракции совершенно бесполезно.
WH>На этом разговор с тобой закончил.

Да, так лучше.

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

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

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

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

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

PD>>Мне бы твои проблемы
S>Я думаю, что от моих проблем ты загнёшся.

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

S>Какая разница, по какой причине ты реализовал "неправильно"? Если "неправильно" — это неконсистентно, то всё обнаружится статической проверкой.

Не смеши.

S>А про "неправильно" в смысле "не решает нужную задачу" я тебе уже ответил: это тебе никакая математика не посчитает.

PD>>Математически обнаружимая... Да, в твоем примере это сойдет. На тебе иной пример — ядро Windows. Спроектируй его в основных чертах и попробуй потом математически обнаружить, а мы посмотрим
S>Ну не странно ли, что для всяческих ОС ядер таки доказывают различные свойства при помощи различных theorem prover-ов?

Угу. А потом тестируют ее сначала у себя (альфа), потом тестируют всем миром бету, потом тестируют всем миром RC, потом тестируют всем миром релиз и пишут хотфиксы и SP. Из чего ясно, какова цена всем этим theorem prover-ов.

S>>>А вот это — тоже вполне себе разрешимая задачка. Если среда умеет выводить и проверять контракты на вычислительную сложность, то ты можешь очень быстро увидеть, где именно боттлнек, еще до запуска профайлера.
PD>>Что я слышу !!! Без профайлера, оказывается, можно. Правда, если среда умеет... А если я сам умею (я могу оценить алгоритм на выч.сложность или уж совсем никак не могу ? — тогда что ?
S>Ну, так ты, наверное, и по регистрам можешь переменные вручную распределить. Но зачем, если компилятор это делает за тебя?

Могу. Не буду, пока не понадобится. Но при чем здесь это ? Ты же так меня за профайлер агитировал и вдруг сам себе противоречишь. Может, все же объяснишь это противоречие ?

PD>>Вроде кто-то утверждал, что надо именно только с профайлером и никак иначе
S>Есть некоторые нюансы.

Ах, все же есть нюансы. Явный прогресс. Еще некоторое время, и ты начнешь понимать, что не все с профайлером делается.


>В частности, автоматически выведенным оценкам производительности я доверяю как-то больше, чем твоим.

А можно показать, где я делал оценки производительности и какова их методика ? Так что не можешь ты им ни доверять, ни не доверять — ты о них ничего не знаешь.

>Из-за сложности алгоритма, превышающншл (допустим) твои способности.

Да, это возможно. Но и тут есть всякие методики, начиная с банальностей (оптимизируйте внутренний цикл), кончая совсем не тривиальными (учет когерентности кэша, выравнивания данных и т.п. ). Но вообще да, я не бог, могу и ошибиться. Профайлер поможет мне эти ошибки найти — я его роль вовсе не отрицал. Но если я априорно заложил o(n^6) там где надо o(n^3) — он не поможет. Впрочем, я тебе это уже не раз говорил.

S>А в общем, из оценки сложности оценить где будет реальный боттлнек далеко не всегда возможно.

Совершенно верно. Не всегда. Но из этого отнюдь не следует, что всегда невозможно.

S>Потому, что равномерных распределений входных данных в природе не бывает. Это ты всегда начинаешь плеваться, когда тебя спрашивают "нет ли у исходной матрицы каких-либо особенностей, благодаря которым её обработку можно было бы ускорить". А умные люди строят, к примеру, оптимизаторы SQL запросов на эмпирическом знании о том, что, к примеру, частоты реальных данных подчиняются распределению Зипфа.

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