Исходное сообщение
"Выпуск Muen 1.0, открытого микроядра для создания высоконадё..." Отправлено Аноним, 26-Окт-21 16:34
> что-то у Вас не сходится - Вы сами пишете, что верификация, которая > выполнялась для Haskel-а, а уже потом был перевод на C, заняла 20 лет. У тех, кто лишь ту новость и читал, но ни по каким сылкам не ходил: http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf > The overallsize of the proof,including framework, libraries, and generated proofs (not shown in the table)is 200,000 lines of Isabelle script. > The abstract spec took about 4 person months to develop > About 2 person years (py) went into Haskell prototype ... > The initial C translation was donein 3 weeks, in total the C implementation took about 2 pm,for a total costof 2.2 py including the Haskell effort. ... > The cost of the proof is higher,in total about 20 py. и с верификацией знаком лишь из заголовка новости - все может быть.

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:	>> что-то у Вас не сходится - Вы сами пишете, что верификация, которая >> выполнялась для Haskel-а, а уже потом был перевод на C, заняла 20 лет. > У тех, кто лишь ту новость и читал, но ни по каким > сылкам не ходил: > http://web1.cs.columbia.edu/~junfeng/09fa-e6998/papers/sel4.pdf >> The overallsize of the proof,including framework, libraries, and generated proofs (not shown in the table)is 200,000 lines of Isabelle script. >> The abstract spec took about 4 person months to develop >> About 2 person years (py) went into Haskell prototype > ... >> The initial C translation was donein 3 weeks, in total the C implementation took about 2 pm,for a total costof 2.2 py including the Haskell effort. > ... >> The cost of the proof is higher,in total about 20 py. > и с верификацией знаком лишь из заголовка новости - все может быть.
	Введите код, изображенный на картинке: