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

Ну использую функциональное программирование уже сейчас.

Самый лучший отзыв, который я читал о Хаскеле, был такой: «Программу хрен заставишь скомпилироваться, но, если она скомпилировалась, она обычно работает правильно». так что, может быть, именно на этом пути лежит успех...

> не закрываются годами

сорри, это я с ХП попутал.
в семерке у них огромнейший прогресс, там они умудрились залатать что-то за 9 месяцев, емнип...

> Ну, с такой-то свободой я вообще могу считать, что у меня машина Тьюринга.

Боюсь, там ты встретишь дух Гёделя :)

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

Если я правильно понимаю, это (в большей степени) благодаря строгой типизации. Лично мне больше нравится Scheme

Самая Ъ ОСь - это ОС главного гуру. Minix'ом её величают. А QNX используют военные, промышленники и люди с организаций, контролируемых МАГАТЭ. Mach используется в Gnu Hurd и в XNU. В XNU его правда извратили, но... А идеи из Mach используются и в FreeBSD(см. управление памятью), и в ядре NT. Среди проприетарных микроядерных ОС есть VxWorks. У меня был рекламный диск с SDK от данной ОС, рекламным материалом и т.д. Система просто чудо. К сожалению этот шедевр и денег стоит:( Военные говорят, от неё просто без ума.

> Поогоди, нечего на линукс пенять, мы его хороним. Где обещанная тобой при доказательстве («мамой клянусь!»)

Смотря, какие спецификации мы пытаемся реализовать. Смотря, что тебе - как заказчику программного комплекса - нужно. Например, аналог OOM Killer-а может быть желанной частью спецификации. Другой вариант: одновременно запускаемые программы должны (исходя из их формально доказанных свойств) все вместе взятые потреблять памяти не больше, чем действительно есть в системе.

вычислимость?

Вычислимость чего?

а что вы хотели от ведра полного дырами дебан как решето?

> А как же ядро QNX? Оно вроде бы тоже fully formally verified, причем давно уже.

Можешь пруфлинк достать?

QNX как раз очень даже живой, с довольно четко обозначенной областью применимости - промышленность и mission-critical системы. Да, на пейс-аналках он не распространен, но он для них и не предназначался.

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

Если я правильно понимаю, это (в большей степени) благодаря строгой типизации.

Я тоже так понимаю %)

Лично мне больше нравится Scheme

«Динамический недоязычок» (c)

> Вычислимость чего?

Того, что задает твой алгоритм, ёпт! Если у тебя нет вычислимости, значит у тебя нет алгоритма.

Я это в мануале к QNX Neutrino читал, пруфлинка, к сожалению, нет под рукой. На http://myqnx.com/ вроде было руководство, в крайнем случае можно раздобыть trial-версию и посмотреть там.

Проигрыватель действительно запыкается. Блин. Действительно DOS. Неприятно. Один кривой процесс так тормознул мою несчастную «флешку» на процессоре Intel Atom. Но ничего не отвалилось. Все работает, правда с тормозами. Наверное ulimit все-таки спас.

> У меня был рекламный диск с SDK от данной ОС, рекламным материалом и т.д. Система просто чудо.

Ты в ней работал? :D

К сожалению этот шедевр и денег стоит:( Военные говорят, от неё просто без ума.

Ггг. Военные, может, и без ума...

> «Динамический недоязычок» (c)

И не говори! Кстати, это чье (с)?

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

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

В чем проблема-то?

Автор - Mauhuur, если память не подводит.

> Давай-ка я перескажу тебе историю про америку. Во входящей в состав ядра Btrfs нашли проблему с неограниченной утечкой дискового пространства, причем указали на проблему алгоритмического характера. В ответ ведущий разработчик btrfs предложил полуработающий патч (примерно как в случае socketpair), и заявил, что болт он клал на все эти алгоритмы. Что сделал Торвальдс? А _ничего_: btrfs по-прежнему в ядре. И со временем его начнут ставить в продакшен. Такой занятный подход к разработке. Там не то что верификация, там ковбои, долбанутые на всю голову.

Это естественный отбор. Со временем таких ковбоев станет меньше. Время покажет, кто ошибался.

Нде, у меня что-то тоже не нагуглилось :(

В процессе установки обновлений проигрыватель стал играть лучше, что натолкнуло на мысль.
Запустил gnome-terminal, в 3 вкладках запустил «cat /dev/urandom >/dev/null» - проигрыватель перестал запыкаться, мышь перестала тормозить, хотя эта дрянь болтается где-то в фоне и не желает подыхать. Все работает практически нормально. Так что аварийное лекарство от этой дряни для тех, кто попробует запустить - создать preemptible kernel load, чтобы отпустило, а потом уже перемонтировать fs в ro и перезагружаться.
Вот такой он интересный этот линукс.

c:your Landic

ЛОР - торт. У новости про упоротого диверсанта с X.org. Помечена как «секурити». А новость про чоткий кернел-эксплоит как «новости ядра». Типа фича? :D

А между делом...

На Хабре товарищ отписался, что CentOS так не кладется (RHEL), соответственно, тоже. С оговоркой, что не под рутом запускать (под рутом падает всё же).

Но, собственно, многие помнят «Подскажите плз, что скрипт делает?» там где ещё в начале вроде «echo 1 2 3 |» или как-то так =)

>быдло

быдлокодеры

говно

индустрия говна

А _ничего_ я взамен не предлагаю. Предлагаю хавать то говно

Если вокруг все воняет - мыться не пробовал?

> Я не могу понять сути твоих возражений.

ОК, поехали

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

1. Кто и как будет писать спецификацию? Спецификация — это всего лишь словесное описание той функции (алгоритма), который должна реализовать программа. Во-первых, даже доказательство _существования_ такого алгоритма может быть в высшей степени нетривиальна, а иногда его (алгоритма) и вовсе не существует, например, проблема эквивалентности слов в полугруппе. Заметим, что тут еще никаких «погромистов» даже еще не появлялось на сцене

2. После этого спецификацию надо «положить» на код. В этот момент возникают интересные проблемы, что компьютер — не машина Тьюринга по причине своего плебейского происхождения: у него нет бесконечной памяти, например и вообще он гогно. В этот момент я лично не уверен в том, что перенос, даже идеальный, не лишит программу «идеологической обоснованности» данной в п.1

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

Теперь вопрос: а что стоят вопли г-на Manhunt, кричащего, что Linux-де говняная поделка студентов-недоучек лишь потому, что там не _доказывают_ алгоритмы?

> Если вокруг все воняет - мыться не пробовал?

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

Ну вот, а вы говорите в Линуксе нету багов. Та всюду они!

> Ну вот, а вы говорите в Линуксе нету багов. Та всюду они!

В линуксе есть баги и их находят... Находят ли их в альтернативных линуксу ОС — вот в чем point спора.

Надо менять подход к написанию сложного ПО. Сколько Вирт про модульность говорил? Про упрощение синтаксических конструкций и т.д.? Сколько лет уже существует Lisp и ФЯ? Если изучить идеи Таннебаума, Вирта, и других отцов-теоретиков, взять лучшее из таких прекрасных технологий как Oberon,Lisp и Squeak(Smalltalk) - можно получить идеальные технологии для создания ОС и сложного ПО. Но все кидаются на мэйнстрим, а он defective by design. Ну, и результат соответсвенно такой-же. А кто будет продвигать перспективные технологии, если это не модно, плохо оплачивается и никому вроде, как и не надо? Пройдут годы, пока до людей начнёт доходить, что что-то не ладно в датском королевстве IT индустрии.

>и не желает подыхать

У меня подох минут через 20-30 работы. Бубунта 10.10. То, что не снимается - баг. А то, что тормозит - эта фича Бубунты.

З.Ы. Ушёл читать инструкции по установке RHEL (CentOS).

З.З.Ы. Капча охренела - у неё буква с ударением!

Нет, но я считаю, что вонять перестанет.

В Linux замеченные дыры исправляются за обозримое время. Я вот послал патч на Intel audio в 2.6.15 - и через две недели в zen-sources (gentoo) оно заработало. Я в любомой тобой Windows дыры не исправляются годами.

> Если изучить идеи Таннебаума, Вирта, и других отцов-теоретиков, взять лучшее из таких прекрасных технологий как Oberon,Lisp и Squeak(Smalltalk) - можно получить идеальные технологии для создания ОС и сложного ПО.

Бугага. Только непонятно, Смоллток предлагается для ОС или для «сложного ПО»?

Ты студент-первогодка на программировании, что ли? Откуда столько пафоса в речах?

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

http://thenextweb.com/microsoft/2010/11/25/new-windows-0-day-exploit-bypasses...

> Кто и как будет писать спецификацию?

Человек.

Спецификация — это всего лишь словесное описание той функции (алгоритма), который должна реализовать программа.

Не словесное, а формальное. Это во-первых.

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

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

Естественно. А порой и вовсе можно доказать, что такого алгоритма НЕ СУЩЕСТВУЕТ. К.О. говорит, что хотелки к программе должны быть вменяемыми.

а иногда его (алгоритма) и вовсе не существует, например, проблема эквивалентности слов в полугруппе

Ох, я прочитал твои мысли. Правда.

После этого спецификацию надо «положить» на код. В этот момент возникают интересные проблемы, что компьютер — не машина Тьюринга по причине своего плебейского происхождения: у него нет бесконечной памяти, например и вообще он гогно.

Нет. Реализующий спецификацию алгоритм уже должен оперировать конечными ресурсами. Если в общем случае тебе нужно неограниченно много ресурсов (памяти, например), то придется пересматривать алгоритм и/или спецификацию (скажем, из «отсортировать массив» в «отсортировать массив, имеющий размер не более мегабайта»). Еще раз: хотелки к программе должны быть вменяемыми.

В итоге, просношавшись годы мы не получим того, что хотели.

Мы получим то, что ведет себя в точности так, как описано в спецификации.

что стоят вопли г-на Manhunt, кричащего, что Linux-де говняная поделка студентов-недоучек лишь потому, что там не _доказывают_ алгоритмы?

Точнее, они их игнорируют и гордятся этим. И не думаю, что эти люди - студенты.

> Oberon,Lisp и Squeak(Smalltalk) - можно получить идеальные технологии для создания ОС и сложного ПО.

Попахивает макосью, которая кстати вторая по дырам после винды. Ну а ФЯ - притча во языцех. Пруф? Поиск в разделе девелопмент по темам срача функциональный подход вс императивный, почти всегда оказывается что большинство тривиальных задач в ФЯП выгоднее решать императивным подходом, и только «марсианские задачи» типа каких нибудь околопарадоксальных рассчетов оказываются чууууточку быстрее, и то ИМХО во многом из-за неоптимальной реализацией в императивных ЯП.

> Еще раз: хотелки к программе должны быть вменяемыми.

Епт, неужели ты не понимаешь, что «вменяемость» — это бомба под алгоритмой, программой и алгоритмом? Что есть «вменяемость», как ее понимать и тем более, верифицировать. А что если на 10 Мб алгоритм невозможен, а на 20 — возможен? Нет, твоя программа «идеальна» в том смысле, что не существует ее материальное воплощение ни в одном из известных физических миров.

> скажем, из «отсортировать массив» в «отсортировать массив, имеющий размер не более мегабайта»

Упреждая вопли и визги, К.О. сообщает, что где это возможно, должна быть описана зависимость между объемом/характером входных данных и потребными ресурсами. Например, для сортировки массива unit32, O(N*log(N)) по процессорным тактам и O(N) по потребляемой памяти. К.О. также сообщает, что вместо букв «O» должны быть конкретные оценки «сверху».

Под ударом сервера, десктопные юзеры дальше фапают на компиз...

Интересно что спажет Линус по этому поводу? =))

>> Помню какую-то книгу читал... Хакеры ядра... Лучшие из лучших...

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

Если ты взял тот же LDD, то там никакого пафоса, всё по делу...

скажет

///fixed

>Если я правильно понимаю, это (в большей степени) благодаря строгой типизации. не совсем. оно требует формальной непротиворечивости программы.

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

И вторая по популярности... где-то здесь есть связь :)

>> Нет содержательных и одновременно пригодных для верификации спецификаций.

Подумай почему. Ты полагаешь спецификацию написать проще чем код?
Или достаточно написать требование в стиле 'система не должна падать' и всё устроится само собой?

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

Код написан без учета того, что его будут верифицировать.

;-) т.е. нужно писать код не так, чтобы работало, а чтобы можно было красивую бумажку потом прилепить?

>... А _ничего_: btrfs по-прежнему в ядре. И со временем его начнут ставить в продакшен. Такой занятный подход к разработке. Там не то что верификация, там ковбои, долбанутые на всю голову.

ССЗБ. Кстати, не расскажете ли, что у нас есть из файловых систем уже сертифицированное и готовое к применению? И что, дают какие-то гарантии, что мои данные не потеряются? Заверните парочку.

> Что есть «вменяемость», как ее понимать и тем более, верифицировать.

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

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

А что если на 10 Мб алгоритм невозможен, а на 20 — возможен?

Если 20 Мб нет, то хотелка невыполнима. Увы. И лучше, если заказчик узнает о невыполнимости на этапе программирования, а не тогда, когда однажды эта потребность в 20 Мб приведет к катастрофе IRL.

Практически в любом софте есть баги.

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

Ну и чего разорались-то? Выйдет патч, причем за пару недель максимум. Всего делов-то. Переживем.

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

> И не забываем о тех проблемах в винде и маке, которые так и не стали известны.

Ага. Помним. И в винде, и маке и конечно в линуксе :)