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

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

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

Я думаю, что вот этим http://www.gdc4s.com/ ребятам нвидия не пригодится)

Ну и это явно не для широкого применения, по крайней мере пока.

Ну и это явно не для широкого применения, по крайней мере пока.

Так шутка же. Но с долей правды. Как только этим ребятам понадобится какая-нибудь CUDA...

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

Во-вторых какие у него интефейсы для модулей? Это ведь не posix насколько я понял?

Не будет царя, анонимусу уже нельзя в новости

Куясе.

Как только этим ребятам понадобится какая-нибудь CUDA

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

Я ничего не понял. Что это такое и зачем оно нужно?

А КАК ВЫ ДОКАЖИТИ КОРЕКТНОСТЬ ПРОВЕРЯТИЛЯ КОРЕКТНОСТИ?!?!?!

А так, конечно, очень впечатляющая новость. Но что такое Isabelle (в тегах)?

! в заголовке говорит, что все должны испытывать эйфорию по поводу данного события?

4.2

первого в мире ядра операционной системы с доказанной корректностью

Доказана не корректность ядра, но соответствие спецификации. Какие дыры в спецификации пока неизвестно.

Это микроядро, модель которого была реализована на Haskell и формально верифицирована. А нужно оно для чего угодно. Хоть новую ОС лепи, хоть гипервизор на его основе (именно это уже сделано, если мне не изменяет память).

первого в мире ядра операционной системы с доказанной корректностью:

Hello_world без ошибок выводит?

The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification. Though interactive, Isabelle also features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, as well as various decision procedures. Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. The Isabelle theorem prover is free software, released under the revised BSD license.

Доказана не корректность ядра, но соответствие спецификации

Разумеется. Формальная верификация занимается исключительно этим.

Да. Это довольно популярная в узких кругах саксесс стори.

Не будет царя, анонимусу уже нельзя в новости

Так он же сейчас Carb_blog4, не?

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

Точно нельзя?

А где можно почитать, почему сделан такой идиотский ход?

Лицензия какая?

А под какой лицензией открыты исходники? В репозитарии выложены GPLv2 и BSD, которые между собой не совместимы.

да ну?

:) Ну вот, всё нормально, а я уж было перепугался, как так.

а как вы докажите что такое корректность.

BSD совместима с GPL, но не наоборот

Внезапно. А всё началось со смены опроса на главной...

Вроде годно, потыкаем на досуге

Не умничай, корректность, в данном случае, это соответствие описанной спецификации, только и всего..

Это негодный анон. Игнорируй его. Хотя ты регистрантишка, ты не умеешь игнорировать.

Ну всё, теперь математики горе-погромиздов, не могущих корректно работающий код без тестирования написать, заклюют.

Вот тут читай Почему анонимусам запретили комментировать новости? и просвещайся, что тебе тут запретили комментировать :) Ладно, ждем царя :)

Я ничего не понял.

Нельзя требовать

BSD совместима с GPL, но не наоборот

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

Думаете почему код из Linux'а не попадает в ядро FreeBSD и наоборот?

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

Но потом его собрали при помощи gcc-4.9.0...

Неужто вендекапец?

Потому что попадает. BSD совместима с GPLv2, то есть код под BSD можно взять и перелицензировать под GPLv2, что было проделано с кодом из OpenBSD(Тео тогда еще гору кирпичей отложил), а вот в обратную сторону совместимости нет, по этой причине в FreeBSD никогда не будет нормального кода. Ну и да, авторы могут хоть 100 лицензий сразу навешивать на свой код, в таких случаях можно выбирать под какой он для тебя, а не визжать, что они несовместимы.

Думаете почему код из Linux'а не попадает в ядро FreeBSD и наоборот?

Код из Linux'а таки попадает в xBSD, только этот код не под GPL. Наоборот тоже бывает.

А да, бсд... «When you want to refer specifically to one of the BSD licenses, please always state which one: the “original BSD license” or the “revised BSD license”.»

Однако на гитхабе лежит LICENSE_BSD2.txt - это 2-clause BSD. Совместима с GPL. http://en.wikipedia.org/wiki/BSD_licenses

Нельзя

код под BSD можно взять и перелицензировать под GPLv2

Нельзя. Однажды BSD — всегда BSD. BSD разрешает делать всё что угодно, но требует указывать что используется код опубликованый под лицензией BSD. В GPL нет такого требования, а дополнительные требования GPL добавлять запрещает.

документальное подтверждение твоим словам, пожалуйста

уже нет)

Оперативно.

Ну и зачем такое самоистязание (написание кода без тестов), когда можно сразу описать спецификацию через BDD и код можно будет писать хоть в пьяном угаре с перерывом на шлюх и кокаин, а тесты будут постоянно держать разрабов в заранее определенном коридоре спецификации?

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

А вот и наркоманы подтянулись...

Бред. BSDL на то и BSDL, что лицензию его форка можно менять — перелицензировать под какой-нибудь Apache или GPL, а то и вовсе запроприетарить (чем активно пользуется сонька).

Щедрый жест.

Аксиома: «В каждой программе есть хотя бы одна „ашипка“» :)

Линуксокапец?

Нельзя. Однажды BSD — всегда BSD.

Ха-ха-ха, ещё один попался.