Evgeny_CD, Архитектор (15.09.2012 01:05, просмотров: 13303)-
- seL4. seL4's implementation is formally (mathematically) proved correct (bug-free) against its specification -> seL4-Based Project --> Evgeny_CD(162 знак., 12.02.2016 00:19 - 00:39, ссылка, ссылка)
- Кто понимает в теме, вдруг кто быстро разберется - как именно они верифицируют код на соответствие спецификациям? - Evgeny_CD(12.02.2016 01:45)
- Д.ARMоед - подскажи, плиз.... - Evgeny_CD(12.02.2016 01:46)
- в режиме прохожего: система подвергается функциональной декомпозиции -> записывается на хаскеле. далее TimeZoneDefault(481 знак., 12.02.2016 13:05,
)
- Спасибо! Да, у них там есть хаскельный код в репозитории, и какой-то кодогенаратор на их собственном DSL. Все это весьма близко к подходам, которые я здесь много лет ковыряю. А именно - программист пишет не "сразу в С", а в некий DSL, который, в Evgeny_CD(147 знак., 12.02.2016 16:28)
- последний тезис упирается в понятие "обратимых вычислений", которые существуют не для всех классов алгебр. для алгебры чёрча - формально не существуют :) TimeZoneDefault(801 знак., 12.02.2016 17:18, )
- Спасибо! "частный случай полупрямого произведения групп." Да, это надо переварить.... - Evgeny_CD(12.02.2016 17:52)
- переварить лучше то, что фичи, представляемые в виде "proved" решений для сегодняшних камней на самом деле таковыми не являются в силу фундаментальных причин. - TimeZoneDefault(12.02.2016 19:46, )
- "Не нее-шь, не продаш" :) - Evgeny_CD(12.02.2016 20:58)
- пральна. осталось понять, как нае..ть всех так, чтобы им это понравилось :)) - TimeZoneDefault(12.02.2016 21:39, )
- пральна. осталось понять, как нае..ть всех так, чтобы им это понравилось :)) - TimeZoneDefault(12.02.2016 21:39,
- "Не нее-шь, не продаш" :) - Evgeny_CD(12.02.2016 20:58)
- переварить лучше то, что фичи, представляемые в виде "proved" решений для сегодняшних камней на самом деле таковыми не являются в силу фундаментальных причин. - TimeZoneDefault(12.02.2016 19:46,
- Спасибо! "частный случай полупрямого произведения групп." Да, это надо переварить.... - Evgeny_CD(12.02.2016 17:52)
- последний тезис упирается в понятие "обратимых вычислений", которые существуют не для всех классов алгебр. для алгебры чёрча - формально не существуют :) TimeZoneDefault(801 знак., 12.02.2016 17:18,
- Спасибо! Да, у них там есть хаскельный код в репозитории, и какой-то кодогенаратор на их собственном DSL. Все это весьма близко к подходам, которые я здесь много лет ковыряю. А именно - программист пишет не "сразу в С", а в некий DSL, который, в Evgeny_CD(147 знак., 12.02.2016 16:28)
- в режиме прохожего: система подвергается функциональной декомпозиции -> записывается на хаскеле. далее TimeZoneDefault(481 знак., 12.02.2016 13:05,
- Д.ARMоед - подскажи, плиз.... - Evgeny_CD(12.02.2016 01:46)
- Еще про нее же. В конце страницы шикарная подборка документов и през. - Evgeny_CD(12.02.2016 00:37, ссылка)
- Ой. eChronos project builds and formally verifies, a small, versatile, high-assurance real-time operating system (OS) for embedded micro-controllers -> •Formal functional specification (completed) Какой-то разрыв шаблона. Evgeny_CD(39 знак., 12.02.2016 00:34, ссылка)
- Не понял, что удивляет-то? - LightElf(12.02.2016 10:56)
- Довольно интересен список поддерживаемого харда ->, есть на редкость интересные платы --> BD-SL-i.MX6 ◦The Sabre Lite i.mx6 board. - Evgeny_CD(12.02.2016 00:28, ссылка, ссылка)
- Кто понимает в теме, вдруг кто быстро разберется - как именно они верифицируют код на соответствие спецификациям? - Evgeny_CD(12.02.2016 01:45)
- Щупали и щупаем. Сыровато пока, писать надо много, в часности драйвера, в основном используем Genode и Fiasco.OC+L4Re. Остальные проекты либо закрыты (например OKL4) или близки к смерти (например Pistachio). - vanner(15.04.2013 21:53, ссылка, ссылка)
- Подборка документов по L4 Evgeny_CD(15.04.2013 21:33)
- Тут уместно вспомнить
знатный срачвысокоинтеллектуальный спор Торвальдса и Таненбаума. Мастер-класс по флейму -> - SciFi(15.09.2012 13:27, ссылка) - [:||||||||||:] Новость ~15-летней давности. - fk0(15.09.2012 11:25)
- Верно, стартовало оно 15 лет назад. Вопрос - а какие большие проекты известны на нем? - Evgeny_CD(15.09.2012 11:26)
- Проект Hurd стартовал ещё раньше. Как и всё прочее связанное с именем Столлмана. Лет на 10 ещё до того. И до сих пор живо. И в отличии от, активно используется. - fk0(15.09.2012 11:35)
- "В 2002 году Ричард Столлман, руководитель проекта GNU, заявил о скором выходе производственной версии Hurd, однако его обещания не оправдались" -> - Evgeny_CD(15.09.2012 14:18, ссылка)
- Есть, однако, debian hurd. Однако я не о hurd, а о том, что другие инициативы FSF вполне живы. В частности GCC или множество утилит для linux (в bsd, например, свои, а в linux из FSF). - fk0(15.09.2012 22:47)
- Утилиты для linux? Исправься, иначе прибежит Столлман и начнёт объяснять, что это утилиты для GNU :-) - SciFi(15.09.2012 22:49)
- Есть, однако, debian hurd. Однако я не о hurd, а о том, что другие инициативы FSF вполне живы. В частности GCC или множество утилит для linux (в bsd, например, свои, а в linux из FSF). - fk0(15.09.2012 22:47)
- "В 2002 году Ричард Столлман, руководитель проекта GNU, заявил о скором выходе производственной версии Hurd, однако его обещания не оправдались" -> - Evgeny_CD(15.09.2012 14:18, ссылка)
- Проект Hurd стартовал ещё раньше. Как и всё прочее связанное с именем Столлмана. Лет на 10 ещё до того. И до сих пор живо. И в отличии от, активно используется. - fk0(15.09.2012 11:35)
- Верно, стартовало оно 15 лет назад. Вопрос - а какие большие проекты известны на нем? - Evgeny_CD(15.09.2012 11:26)
- Коммерческая ветвь под BSD лицензией -> На первый взгляд, довольно интересно! - Evgeny_CD(15.09.2012 01:12, ссылка)
- seL4. seL4's implementation is formally (mathematically) proved correct (bug-free) against its specification -> seL4-Based Project --> Evgeny_CD(162 знак., 12.02.2016 00:19 - 00:39, ссылка, ссылка)