All streams
Search
Write a publication
Pull to refresh
4
0
Send message

По расчетам вы платите, не больше 15K$ в месяц программисту из гугла, который пишет 100 строк в день, или 2 000 в месяц, то есть 15 000/2 000, 8$ долларов за строчку. Даже если мы возьмем общий цикл разработки, пусть выйдет 15$, это оценка сверху, в реальности разница будет приближаться к двум десятичным порядкам. (15$ vs 1000$)

  1. Вы не можете, просто проверить все состояния модуля, так как это неизбежно ведет к комбинаторному взрыву, если это что-то сложнее тривиального. Даже банальная сортировка - уже нет. А так unit тесты придумали, очень давно, кто-то делает по другому?

  2. Запрос есть, и он огромный со стороны aero-space никто не хочет платить 500$ за строчку, проблема в том, что в отличии от железнячных RTL абстракций, где все цветет и пахнет. Это не решается, с точки зрения алгоритмов и математики. А то что решается, не интересно промышленности.

>Кстати, верхний результат по запросу program verification sorting

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

Тоесть вы готовы платить 500$ за строчку в софте? Оценка, более чем реальная, с прувингом дешевле не выйдет. Еще проблема в том, что стоимость верификации растет очень нелинейно. Это все работает, хоть как-то, если вы готовы жить в мире 10К строчников, и некоторых простых их взаимосвязей. Любой Model-checker для софта работает достаточно просто - это полный перебор пространства возможных состояний, на чем-то сложнее, определенного предела, они просто взрываются. Даже простую сортировку вы в модел чекере не верифицируете.

PS: и главное, у меня нет уверенности, что это действительно для большого софта, лучше чем требование покрытия (code coverage) на 99%, которое будет стоить на два порядка дешевле.

Все уже давно придумано до нас, и решается в общем случаи, https://en.wikipedia.org/wiki/Birth–death_process не надо велосипедов.

По моей ссылке на seL4 верификацией занимался очень крутой институт, результат - 4 тыщи строк кода и 3 года времени. С оценкой 400$-1000$ за строчку кода. К слову в seL4, agda и не было близко, плохо представляю как на ней можно было бы доказать корректность ядра ОС, где сплошные сайд эффекты, но с вопросом я не знаком.

По ссылке, которой вы дали, вообще model-checker. Это совершенно другой подход, он принципиально не масштабируется на глобальную проверку корректности, если только ни чтото совсем маленькое.

Дело ни в том, что пишет тот кто точно знает. В крипте, тоже были уязвимости, тот же heartbleed, да и еще менее известные. Про видеокодеки, вы просто не знаете, потому что это никак на вас не влияет, ну дернулось изображение чуток, запороть кодек до сегфолта сложно, так как это вск покрывается тестами. Ну и все о чем вы говорите уже стабильно лет 10.

По поводу пространства состояний вы, конечно хватили, даже для банального инта оно будет 2^32.

Если интересно, посмотрите https://en.wikipedia.org/wiki/L4_microkernel_family#High_assurance:_seL4 там есть и оценки того, сколько стоит строчка кода "без багов".

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

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

Ну и стоить этот софт будет в 100 раз больше. Тем более никто не дает гарантии, что соединение этих IP блоков, то есть обвязка не будет содержать ошибок. В софте, тем более все, более печально в плане верификации, чем с железом.

PS: весь этот отказ от гарантии не просто так сделан. Если нужна гарантия покупайте софт, который это дает. У кого ни буть из aero-space, только стоить оно будет как чугунный мост.

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

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

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

Списки составлялись в чатике it мобилизации(ITmobilization) в телеге, все выходные, внесли всех кого смогли.

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

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

Их и так будет немного, в отрасли 0.5 млн мужчин, с профильным ВО процентов 20-30 максимум. Если им хоть както удастся помочь уже хоть что-то. Защитник прав человека, конечно, фантасмогоричный получился.

Там отдельный столбец надо, может ли сортировка в inplace или нет, или указывать асимптотику дополнительной памяти.

Это понятно, вопрос конвергенции. Мне лично не ясно, чем metal принципиально лучше vulcan. Просто apple может тащить очередной стандарт без "фатальных ошибок".

Отлично расскажите какие такие специфичные механизмы на уровне ядра ОС(которая к тому же unix подобная), нужны для драйвера видеокарты процентов 90 которого находится в юзер-спэйс? А то мне прямо интересно стало.

Картинка как раз в тему, если бы их волновали именно технологии современного рендера то там бы был Vulkan, а OpenGL можно оставить для кучи всякого легаси. А так - очередной вендор лок, приправленные лапшей которую надо снять с ушей.

Очень фантастично. ) Зачем им держать людей под контролем если у них есть роботы, которые и так все сделают?

На данном этапе развития ИИ(machine learning) говорить, что нас захватит ИИ, все равно утверждать, что нас захватит синус с косинусом.

Information

Rating
Does not participate
Registered
Activity

Specialization

Software Developer, Application Developer
Senior
C++
C++ STL
Linux
Python
Machine learning
Applied math
Algorithms and data structures
Code Optimization