История изменений

Я желаю вам всяческих успехов и сам буду рад

Спасибо большое, аналогично.

… как будто есть фундаментальная причина, почему доказывать … что-нибудь полезное вроде «в корзину заказа могут попадать только имеющиеся на складе товары» — не выходит.

Гм. Ну, по формальной верификации, это, конечно, большое спасибо за вопрос :)

Так как я имею какое то отношение к формальной верификации, то я пожалуй попробую ответить и постараюсь изложить эту причину.

Часто люди которые не слишком углублялись в вопрос видят формальную верификацию как некую не вполне понятную альтернативу тестированию при разработке ПО. Нужно сказать, что по крайней мере на данный момент это в, целом, ошибочное мнение. Формальная верификация не заменяет тестирование и не отменяет его. Может быть когда-то в будущем подходы разовьются и получится разрабатывать верифицированный код или может быть Type Driven Development от Edwin Brady получит распространение, что [пмсм] гипотетически сильно сократит количество тестов... но это всё не сегодня.

На сегодняшний день формальная верификация - это очень надёжный аудит. Применяется там же где аудит и тогда же когда аудит. Только с дополнительными требованиями вида «чтобы ни одна мышь». Соответственно, удовольствие не из дешёвых.

Теперь мне кажется уже довольно очевидным, что из вопроса «А много ли корзин заказа которые отдавали на аудит вы видели?» и ответа на него в виде цифры ноль отнюдь не следует фраза ниже

Рад буду ошибиться, но … как будто есть фундаментальная причина, почему *провести аудит на тему* «данная булевая функция удовлетворяет таким-то критериям» получается, а для чего-нибудь полезного вроде «в корзину заказа могут попадать только имеющиеся на складе товары» — не выходит.

Отчасти просто потому на самом деле что вы не там смотрите. Попробуйте например набрать в поисковике «formal verification of smart contracts».

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

А если вдруг Фобос вместо того чтобы в грунт околомарсианский врезаться, врежется в гладь водную на Земле, то тоже ничего. Бывает. (правда я так и не понял что у них случилось, говорили расчёты там где то запороли, но как именно в прессе я не видел).

За вопрос - большое спасибо ещё раз :)

Я желаю вам всяческих успехов и сам буду рад

Спасибо большое, аналогично.

… как будто есть фундаментальная причина, почему доказывать … что-нибудь полезное вроде «в корзину заказа могут попадать только имеющиеся на складе товары» — не выходит.

Гм. Ну, по формальной верификации, это, конечно, большое спасибо за вопрос :)

Так как я имею какое то отношение к формальной верификации, то я пожалуй попробую ответить и постараюсь изложить эту причину.

Часто люди которые не слишком углублялись в вопрос видят формальную верификацию как некую не вполне понятную альтернативу тестированию при разработке ПО. Нужно сказать, что по крайней мере на данный момент это в, целом, ошибочное мнение. Формальная верификация не заменяет тестирование и не отменяет его. Может быть когда-то в будущем подходы разовьются и получится разрабатывать верифицированный код или может быть Type Driven Development от Edwin Brady получит распространение, что [пмсм] гипотетически сильно сократит количество тестов... но это всё не сегодня.

На сегодняшний день формальная верификация - это очень надёжный аудит. Применяется там же где аудит и тогда же когда аудит. Только с дополнительными требованиями вида «чтобы ни одна мышь». Соответственно, удовольствие не из дешёвых.

Теперь мне кажется уже довольно очевидным, что из вопроса «А много ли корзин заказа которые отдавали на аудит вы видели?» и ответа на него в виде цифры ноль отнюдь не следует фраза ниже

Рад буду ошибиться, но … как будто есть фундаментальная причина, почему *провести аудит на тему* «данная булевая функция удовлетворяет таким-то критериям» получается, а для чего-нибудь полезного вроде «в корзину заказа могут попадать только имеющиеся на складе товары» — не выходит.

Отчасти просто потому на самом деле что вы не там смотрите. Попробуйте например набрать в поисковике «formal verification of smart contracts».

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

За вопрос - большое спасибо ещё раз :)

Я желаю вам всяческих успехов и сам буду рад

Спасибо большое, аналогично.

… как будто есть фундаментальная причина, почему доказывать … что-нибудь полезное вроде «в корзину заказа могут попадать только имеющиеся на складе товары» — не выходит.

Гм. Ну, по формальной верификации, это, конечно, большое спасибо за вопрос :)

Так как я имею какое то отношение к формальной верификации, то я пожалуй попробую ответить и постараюсь изложить эту причину.

Часто люди которые не слишком углублялись в вопрос видят формальную верификацию как некую не вполне понятную альтернативу тестированию при разработке ПО. Нужно сказать, что по крайней мере на данный момент это в, целом, ошибочное мнение. Формальная верификация не заменяет тестирование и не отменяет его. Может быть когда-то в будущем подходы разовьются и получится разрабатывать верифицированный код или может быть Type Driven Development от Edwin Brady получит распространение, что [пмсм] гипотетически сильно сократит количество тестов... но это всё не сегодня.

На сегодняшний день формальная верификация - это очень надёжный аудит. Применяется там же где аудит и тогда же когда аудит. Только с дополнительными требованиями вида «чтобы ни одна мышь». Соответственно, удовольствие не из дешёвых.

Теперь мне кажется уже довольно очевидным, что из вопроса «А много ли корзин заказа которые отдавали на аудит вы видели?» и ответа на него в виде цифры ноль отнюдь не следует фраза ниже

Рад буду ошибиться, но … как будто есть фундаментальная причина, почему *провести аудит на тему* «данная булевая функция удовлетворяет таким-то критериям» получается, а для чего-нибудь полезного вроде «в корзину заказа могут попадать только имеющиеся на складе товары» — не выходит.

Просто потому на самом деле что вы не там смотрите. Попробуйте например набрать в поисковике «formal verification of smart contracts».

За вопрос - большое спасибо ещё раз :)