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

M>Даже если отбросить вопросы производительности, оперировать напрямую с указателями мне просто удобнее по той причине, что об этом просто не надо задумываться.
А кто же обещал простых путей? За определенные удобства в одном нужно платить выкрутасами в другом (происходит ломка). Но это тоже интересно, плюс изменение мышления.
Пока, что JIT далек от совершенства. Но все течет,все меняется и у манагед в перспективе аппаратная независимость на уровне байт кода.
Да еще плюс ParallelFx

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

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

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

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

PD>>Можешь сделать, чтобы не было доступа куда не надо, модификации чего не надо, но если вместо плюса в ней минус, то это отловить тебе никто не поможет.
S>Я, в общем-то, согласен и на 99%.

Я так думаю, что придется на 100%. Потому что этот плюс там не по ошибке, а мне именно так и надо, как выяснилось

PD>>Имеешь право хотеть. Заодно создай себе гарантии, что все прочие exception тоже никогда возникать не будут. Теоретически это, наверное, возможно, практически не существует и едва ли интересно.
S>Видишь ли, уровень безошибочности, достижимый при помощи K&R С, был достигнут уже давно. И мне как раз неинтересно рассуждать на тему "а потому работай-не работай, всё едино".
S>Мне интересно думать на тему "а что еще можно улучшить?"

Многое можно улучшить, хотя при чем тут K&R — неясно. Но то, что вы улучшаете (index out of range, access violation и т.д.) есть маленький-маленький процент от числа всевозможных ошибок при мало-мальски серьезном алгоритме. Поэтому мне и не кажется серьезным такая забота об этих мелочах. Серьезные вещи вы все равно не улучшите, так как неформализуемо это (см. пример с плюсом-минусом, а это самый примитивный из тех, что я могу придумать)

PD>>Меня это мало интересует. Меня гораздо больше интересует суть алгоритма, чем нештатные ситуации. Их обработка в конечном счете пишется в большинстве случаев почти не думая, а сколько там будет строк — мне все равно, я и так знаю, что я на это потрачу намного меньше времени, чем на собственно решение задачи.
S>Просто в твоих задачах, значит, эти ситуации малосущественны.

Да.

PD>>Под ограниченностью я имею в виду, что вы накладываете серьезные требования на иммутабельные типы, а поэтому большинство типов таковыми не будет.
S>Да ладно! Это ты как считал?

Я никак не считал, но приведи мне эти самые иммутабельные типы в нынешней библиотеке. String, DateTime... сколько еще покажешь общеупотребимых ?

PD>>И дело здесь не в будущем, а в существе — мы все же в программе имеем намного больше переменных, чем констант, пусть и временно живущих.
S>Гм. Как бы так тебе объяснить... Ты под термином "программа" всё время подразумеваешь "программа на языке С".

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


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

См. мой ответ WolfHound в самом конце.

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

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

PD>>Не ядро системы, а сама система, равно как и все прочие приложения. Только нарушитель изгоняется. И мне как пользователю этой машины это очень даже интересно — я вовсе не хочу после каждого падения программы нажимать на Reset. Не хочу обратно в ДОС
WH>А ДОСа не будет. Система будет более устойчивой чем сейчас.
WH>Если в неком процессе будет ошибка то можно просто прибить этот процесс и все.

И сейчас можно.

WH>Система как работала так и будет работать.

И сейчас работает.

WH>Причем это касается не только рядовых процессов как в венде, а всех включая драйверы.

Да, вот тут ты прав. Жаль, что идея 4 колец не реализовалась. Драйверы ИМХО не должны бы быть в нулевом кольце, а должны бы в 1-м. Тогда при ошибке в драйвере ядро могло бы его прибить. В общем, модель 80286. Но не пошло.

S>>>Интересно иметь до начала выполнения программы гарантии того, что даже и попыток выполнить недопустимую операцию не будет.
PD>>Ха! А гарантии , что файл на диске есть, ты не хочешь ?
WH>Лично я хочу но не очень понятно как этого добиться.

А зачем ? Что все же плохого просто в том, чтобы проверить наличие файла ?

PD>>Почему же тебя уставивает FileNotFoundException (и другие), но не устраивает AccessViolationException ?
WH>По тому что от FileNotFoundException не избавится, а вот без AccessViolationException можно спокойно жить.

И что ? Что вы все эти пустяки раздуваете до немыслимых размеров , а потом борьбу с ними представляете как чуть не главное в программировании. Ну пустяки это же все. Мелочи.

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

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

PD>>Да я не против самой идеи статической верификации. Но ИМХО слишком дорого вы за нее платите
WH>Чем конкретно мы за нее платим?
WH>Отказом от С++? Ну да и хрен бы с ним.

PD>>и слишком она ограничена.
WH>А конкретно?

Давай так. Я не имею времени обсуждать все это с тобой и Антоном одновременно. Либо вы скооперируйтесь, либо смотри мои ответы не только в ответе тебе. Я ему ответил.

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

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

PD>>Все, теперь все стало ясно. Вирусы пролезают в нулевое кольцо из-за того, что защита поставлена не каждому байту, а всем 4К одинаковая
WH>А ты что не знал?
WH>Переполнили буффер и вперед.

Да ну ? А можно поподробнее, как это можно переполнить буфер и проникнуть таким образом в нулевое кольцо ? Можно примерчик кода 3 кольца ? Или это только вирусописатели умеют так буфер переполнять ?

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

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

S>Пока, что JIT далек от совершенства. Но все течет,все меняется и у манагед в перспективе аппаратная независимость на уровне байт кода.

Аппаратную независимость можно достичь и на уровне исходников. По крайней мере принципиальных отличий байт-кода от исходников нет. По идее один и тот же C# код должен компилироваться в один и тот же байт-код. Так что большой разницы нет, то ли я получу байт-код, то ли я получу код на C#. Так что претензии больше не к самой идее JIT, а к требованию верифицируемости кода. Да, верификация нужна больше в тех случаях, когда код запускается без моего ведома, как, например, скрипты на странице. Но в этом случае, по большому счету, и не нужна производительность. А если я скачал программу из интернета, я доверяю ее автору. Откомпилировал да запустил, и на верификацию плевать. И пример больше иллюстрировал тот факт, что разрабатывать неверифицированный код в некоторых случаях проще. Ну и, собственно говоря, непонятно, почему верифицированный код должен вытеснить неверифицированный?

В дополнение.

Я тебе серьезно советую — разберись наконец, чем виртуальная память отличается от физической , и кто чем управляет. Не в твоей гипотетической управляемой ОС, а в Windows. Ты их просто-напросто путаешь, а поэтому пишешь такое, что ни в какие ворота не лезет.

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

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

Что-то мы начали подпевать друг другу.

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

PD>Ты сначала разберись, чем отличается виртуальная память от физической (включая своп),
Я это понимаю не хуже тебя.

PD>чтобы не говорить такое.
Какое такое?

PD>То, о чем ты говоришь, есть управление физической памятью в ОС, своп файл и RAM исключительно под ее контролем, я туда никак из 3 кольца попасть не могу. А сборка мусора есть действие исключительно в виртуальной памяти процесса.
Почему исключительно?

PD>А если не секрет, как из программы 3 кольца узнать, как давно мы не обращались к этой странице ?
А ей и не надо.
Хачим ОСь и вперед.
Мир одной виндой не ограничен.

PD>Юмор могу и оценить, но честное слово, кончай высказываться по вопросам, в которых ты не разбираешься! У тебя есть области, в которых ты разбираешься неплохо, зачем тебе лезть туда, где ты ничего не понимаешь и говорить чепуху ?
А может это ты не понимаешь?

PD>И все же, если в формуле для корней квадратного уравнения я напишу sqrt(b*b+4*a*c), какие зависимые типы это отловят ? А может, мне именно так и надо ?
Я не сказал все.
Я сказал многое.

PD>Да все можно — в теории.
Почему в теории?
Языки с зависимыми типами делают это на практике.

PD>И твоя тотально управляемая ОС в теории тоже не так уж плоха. Как идея. Но реально тебе накидали немало возражений (DMA, текстуры, внешние устройства), могу еще и свое добавить — CUDA, там надо резидентную память иметь.
Только куберакс сам признал что там все будет не хуже чем сейчас...

PD>И т.д. И практически чтобы твою идею о тотальном управлении реализовать, нужен иной процессор, иная периферия, в общем, глобальная революция.
Единственное что нужно изменить в современном железе это добавить IOMMU.
Все!
А его уже добавляют...

PD>А ты чем заплатишь ? Некоторой (и то в теории, никто же не проверял) надеждой на улучшение надежности программ, которые не будут лезть куда не надо ?
Ну почему же в теории?
Даже тупая жаба и та демонстрирует вполне себе приличные результаты.

PD>И ради этого переписать все ПО, переделать всю аппаратуру ? И ради этого миллиарды долларов ? Не дадут.
ПО можно переделывать постепенно. Ведь можно начать с относительно небольших ниш.
Тем более что начать можно даже не с полноценной ОС, а с виртуальной машины типа жабы. А когда программ будет достаточно можно уже и в полноценную ОС превращаться. Да и смешанный вариант тоже доступен.
Железо подойдет современное.
Даже без IOMMU но тогда периферии придется доверять. В прочем в современных ОС ей и так доверяют.

PD>Именно. Я же об этом и говорю. Разные есть задачи. А машина одна
А процессор один.
Ты сказать то что хотел?
Что нештатные ситуации обрабатывать не надо?

PD>Так разные же есть задачи. Вот ты писал, как говоришь, числодробилки. Там констант много было ? Как бы все не кончилось 4 константами — 0 , 1 pi и e
Числомолотилки прекрасно пишутся на функциональщине при наличии оптимизатора.
А есть и более интересный базис.
Абстрактная сетевая машина называется.
Одно из свойств этого базиса частичные вычисления, а это ключ к очень мощной оптимизации.
Другое замечательное свойство это независимость результата от порядка вычислений, а это ключ к распараллеливанию.

А еще у меня есть чувство что сплав АМС и зависимых типов будет практически идеальным базисом для произвольных DSL.

PD>Так, стоп. Под переменными я имею в виду отнюдь не описания
PD>List* pL;
PD>безусловно формально одна переменная, но в действительности их тут столько, сколько полей у всех элементов списка.
И чё?
У меня и в таком свете переменных мало.

PD>Я с немерле не знаком, поэтому спорить не буду. Но по существу, думаю, они и там есть, хотя формально, может, и нет.
Не надо думать. Надо знать.
Вот например простенький оптимизатор без единой переменной.

  partial internal class Optimizer
  {
    public static CanInline(name : string, grammar : Grammar) : bool
    {
      def canInline(rule, recRules)
      {
        match (rule : Rule)
        {
        | Call(name)               =>
          if (recRules.Contains(name))
            false;
          else
            canInline(grammar.GetRule(name), recRules.Add(name));
        | Choice(rules)            => rules.ForAll(rule => canInline(rule, recRules));
        | Sequence(rules)          => rules.ForAll(rule => canInline(rule, recRules));
        | Capture(_, rule)         => canInline(rule, recRules);
        | RepeatMin(_, rule)       => canInline(rule, recRules);
        | RepeatMinMax(_, _, rule) => canInline(rule, recRules);
        | Not(rule)                => canInline(rule, recRules);
        | And(rule)                => canInline(rule, recRules);
        | Chars                    => true;
        | ExtensionPoint           => true;
        }
      }
      canInline(grammar.GetRule(name), Set().Add(name));
    }

    public static OptimizeRule(rule : Rule, grammar : Grammar) : Rule
    {
      def optimize(_ : Rule)
      {
      | Choice(rules) =>
        def rules = rules.Map(optimize);
        def rules = rules.Map(fun(_)
        {
        | Rule.Choice(rules) => rules;
        | rule => [rule];
        });
        def rules = rules.Flatten();
        def catChars(_)
        {
        | Rule.Chars([chars1]) :: Rule.Chars([chars2]) :: rules =>
          catChars(Rule.Chars([chars1.Sum(chars2)]) :: rules);
        | rule :: rules =>
          rule :: catChars(rules);
        | [] => [];
        }
        def rules = catChars(rules);
        match (rules)
        {
        | [rule] => rule;
        | _      => Rule.Choice(rules);
        }

      | Sequence(rules) =>
        def rules = rules.Map(optimize);
        def rules = rules.Map(fun(_)
        {
        | Rule.Sequence(rules) => rules;
        | rule => [rule];
        });
        def rules = rules.Flatten();
        def catChars(_)
        {
        | Rule.Chars(chars1) :: Rule.Chars(chars2) :: rules =>
          catChars(Rule.Chars(chars1.Append(chars2)) :: rules);
        | rule :: rules =>
          rule :: catChars(rules);
        | [] => [];
        }
        def rules = catChars(rules);
        match (rules)
        {
        | [rule] => rule;
        | _      => Rule.Sequence(rules);
        }

      | RepeatMin(min, rule)         => Rule.RepeatMin(min, optimize(rule));
      | RepeatMinMax(min, max, rule) => Rule.RepeatMinMax(min, max, optimize(rule));

      | Not(Not(rule))         => optimize(Rule.And(rule));
      | And(Not(rule))         => optimize(Rule.Not(rule));
      | Not(And(rule))         => optimize(Rule.Not(rule));
      | And(And(rule))         => optimize(Rule.And(rule));
      | Not(rule)              => Rule.Not(optimize(rule));
      | And(rule)              => Rule.And(optimize(rule));

      | Capture(name, rule)    => Rule.Capture(name, optimize(rule));
      | Chars as rule          => rule;
      | ExtensionPoint as rule => rule;

      | Call(name)             =>
        if (CanInline(name, grammar))
          optimize(grammar.GetRule(name));
        else
          Rule.Call(name);
      }
      optimize(rule);
    }
  }

Написать это короче практически невозможно.

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

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

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

S>ты же сам сказал, что верификацией должен заниматься компилятор.
Ага. Компилятор из промежуточного кода в нативный...

S>компилятор работает не на твоей машине
frontend да.
А вот backend на моей.

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

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

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

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

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

WH>>А ДОСа не будет. Система будет более устойчивой чем сейчас.
WH>>Если в неком процессе будет ошибка то можно просто прибить этот процесс и все.
PD>И сейчас можно.
WH>>Система как работала так и будет работать.
PD>И сейчас работает.
Я жэто все к тому что ДОСа не получится.

PD>Да, вот тут ты прав. Жаль, что идея 4 колец не реализовалась. Драйверы ИМХО не должны бы быть в нулевом кольце, а должны бы в 1-м. Тогда при ошибке в драйвере ядро могло бы его прибить. В общем, модель 80286. Но не пошло.
Ага. По тому что тормозило...
А в случае программной изоляцией никаких колец не нужно вообще.
При том что логических слоев защиты может быть сколько угодно.

WH>>Лично я хочу но не очень понятно как этого добиться.
PD>А зачем ? Что все же плохого просто в том, чтобы проверить наличие файла ?
Чтобы не забыть проверить и не придумывать потом что делать если его таки нет.
Пойми одну простую вещь: Гарантировать отсутствие проблема гораздо лучше чем решать последствия проблемы.

PD>И что ? Что вы все эти пустяки раздуваете до немыслимых размеров , а потом борьбу с ними представляете как чуть не главное в программировании. Ну пустяки это же все. Мелочи.
Избавление от всех исключений не вызванных внешними факторами мелочи?
Проверка кода на уровне до которого юниттестам как до пекина раком мелочи?
Уничтожение вирусов мелочи?
...
Фигасе у тебя мелочи.

PD>При чем тут менеджер памяти ОС, когда я говорю о произошедшем в моем процессе исключении, которое я хочу обработать (SEH) и продолжать.
А у меня этого исключения гарантированно не будет.

PD>А тебе известно, что я могу вполне сознательно допускать Access Violation, ибо он часть логики моей программы и именно этого я и хочу ?
А нахрена оно тебе нужно? Что это за логика такая?

PD>Посмотри у Рихтера, там это обсуждается (в разделе по управлению виртуальной памятью). И вообще ты про резервирование и коммитирование слышал, чем отличаются, понимаешь ?
Не хуже тебя.

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

PD>Да ну ? А можно поподробнее, как это можно переполнить буфер и проникнуть таким образом в нулевое кольцо ? Можно примерчик кода 3 кольца ? Или это только вирусописатели умеют так буфер переполнять ?
А сразу в нулевое кольцо и не надо.
Сначала вломились в какой нибудь браузер.
Потом устроили эскалацию привилегий.
Потом поставили драйвер.
...

В управляемой ОС все останется на стадии не смогли вломиться в браузер.

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

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.64

Аж до экспоненциальной сложности доходит для определённых логик.

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

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

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

WH>Потом просто разбиваешь Int64 на байты и...

Это сможет как-то соперничать по скорости. И то надо измерить как, потому что BSF/BSR будет все равно быстрее. И еще нужно ломать голову над тем, чтобы сделать запись такой же выразительной. Во-вторых, тот магический код, что я приводил

Автор: Mystic
Дата: 23.06.09

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

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

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

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

S>Хотя для мобильных устройств на первоначальном этапе, верифицированый код может дать множество бенефитов
1)Для любых.
2)На всех этапах.

S>(оберон системы для беспилотных аппаратов работают).
Это настолько тепличная среда что обсуждать тут нечего.

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

S>>А по поводу, что проще никто и не спорит. Но когда разговор идет об отказоустойчивости, то верификации стоит уделить больше внимания. В свое время Оберон системы много здесь обсуждались, причем достаточно надменно, затем появилась сингулярити и тон уже сильно изменился.
WH>А что в оберон системах уже завелся верифицируемый код?
На уровне комплятора. Там манагед языки
WH>А может там появились зависимые типы?
Дай ссылки на зависимые типы, а тупой найти не могу.
WH>Или они наконец избавились от идиотской идеи одного логического пространства на всех?
WH>А может они еще и от глобальных переменных избавились?
Ну идея SIP практически та же, но не знаю ка в обероне с изоляцией процессов. Опять же Exchange Heap
имеет место жить. Ну и последующие Оси должны все же сильно отличатся от того, что сделал Вирт с сотоварищами, при скудном финансировании,
и теоретической базы. От простого к сложному.
S>>Для разных задач нужны различные инструменты.
WH>Для чего конкретно не подходит верифицируемый код?
Надо говорить об эффективности на конкретном временном отрезке.

S>>Хотя для мобильных устройств на первоначальном этапе, верифицированый код может дать множество бенефитов
WH>1)Для любых.
WH>2)На всех этапах.

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

S>>(оберон системы для беспилотных аппаратов работают).
WH>Это настолько тепличная среда что обсуждать тут нечего.
Работающая, но по 3 рубля.

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

T>http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.29.64
Статейка как я понимаю платная...
Даже мой любимый обесплатниваетель http://scholar.google.com/ что-то не помогает.

T>Аж до экспоненциальной сложности доходит для определённых логик.
Да и причем тут Unrestricted Hierarchical State Machines ?
Вот скажем взяли программу на хаскеле.
Рассахарили, вывели все типы,...
И результат сбросили в бинарник.
Лично я не вижу ни одной причины по которой верификация этого бинарника требовала бы отличное от O(N) время.

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

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

WH>>А может там появились зависимые типы?
S>Дай ссылки на зависимые типы, а тупой найти не могу.
Уже давал. http://en.wikipedia.org/wiki/Dependent_type
Ты ветку не читаешь что-ли?

WH>>Или они наконец избавились от идиотской идеи одного логического пространства на всех?
WH>>А может они еще и от глобальных переменных избавились?
S>Ну идея SIP практически та же,
Нет у оберонщиков SIP. Совсем нету.

S>но не знаю ка в обероне с изоляцией процессов.
Никак.

S>Опять же Exchange Heap имеет место жить.
Деталь реализации которой может и не быть. По крайней мере в том виде в каком оно есть в сингулярити.
В любом случае работа с Exchange Heap гораздо более упорядочена чем садом и гамора оберонщиков.

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

WH>>Для чего конкретно не подходит верифицируемый код?
S> Надо говорить об эффективности на конкретном временном отрезке.
Отрезке чего?

S> Которых еще не существует. А двигаться лучше от простого к сложному, тем более уже есть в этом направлении наработки.
Какие? Только не надо про совершенно непотребную оберон ось.

S>>>(оберон системы для беспилотных аппаратов работают).
WH>>Это настолько тепличная среда что обсуждать тут нечего.
S> Работающая, но по 3 рубля.
Чё?