Вариант для распечатки		Пред. тема | След. тема
Форум Разговоры, обсуждение новостей
Изначальное сообщение		[ Отслеживать ]

"Увидел свет Debian GNU/Hurd 2017"	+/–
Сообщение от opennews (??), 18-Июн-17, 21:30
Представлен (https://lists.debian.org/debian-hurd/2017/06/msg00017.html) релиз Debian GNU/Hurd 2017, редакции дистрибутива Debian 9.0 "Stretch" (https://www.opennet.ru/opennews/art.shtml?num=46713), сочетающей программное окружение Debian c ядром GNU/Hurd. Репозиторий Debian GNU/Hurd включает примерно 80% пакетов от общего размера архива Debian, в том числе портированы Firefox и Xfce 4.12. Debian GNU/Hurd и Debian GNU/KFreeBSD являются единственными платформами Debian, созданными на базе ядра, отличного от Linux. Платформа GNU/Hurd не вошла в число официально поддерживаемых архитектур Debian 9, поэтому релиз Debian GNU/Hurd 2017 выпущен отдельно и имеет статус неофициального выпуска Debian. Готовые сборки, снабжённые специально созданным графическим инсталлятором, и пакеты в настоящее время доступны только для архитектуры i386. Для загрузки подготовлены (http://ftp.ports.debian.org/debian-ports-cd/hurd-i386/debian.../) установочные образы NETINST, CD и DVD, а также образ для запуска в системах виртуализации. GNU Hurd представляет собой ядро, развиваемое в качестве замены ядра Unix и оформленное в виде набора серверов, работающих поверх микроядра GNU Mach и реализующих различные системные сервисы, такие как файловые системы, сетевой стек, система управления доступом к файлам. Микроядро GNU Mach предоставляет IPC-механизм, используемый для организации взаимодействия компонентов GNU Hurd и построения распределённой мультисерверной архитектуры. В новом выпуске ядро GNU Hurd и микроядро GNU Mach обновлены до последних версий 0.9 и 1.3 (https://www.opennet.ru/opennews/art.shtml?num=45713), примечательных заметным повышением стабильности и переработанной системой управления памятью. Значительно расширены возможности утилиты fakeroot, которую можно использовать для быстрой и безопасной сборки пакетов. В качестве варианта легковесной виртуализации добавлена поддержка запуска вложенных hurd-окружений от непривилегированного пользователя. Добавлена поддержка работы с более чем 3 Гб ОЗУ. URL: https://lists.debian.org/debian-hurd/2017/06/msg00017.html Новость: http://www.opennet.ru/opennews/art.shtml?num=46719
Ответить | Правка | Cообщить модератору

Сообщения

[Сортировка по времени | RSS]

1. "Увидел свет Debian GNU/Hurd 2017"	–5 +/–
Сообщение от Аноним (-), 18-Июн-17, 21:30
> Debian GNU/Hurd и Debian GNU/KFreeBSD являются единственными платформами Debian, созданными на базе ядра, отличного от Linux. Это неправда. См. https://www.osdyson.org
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	3. "Увидел свет Debian GNU/Hurd 2017"	+7 +/–
	Сообщение от Аноним (-), 18-Июн-17, 21:48
	Dyson левый дистрибутив на базе Debian, как и NexentaStor, а в новости речь об платформах Debian, развиваемых в рамках основного проекта.
	Ответить | Правка | ^ к родителю #1 | Наверх | Cообщить модератору

	4. "Увидел свет Debian GNU/Hurd 2017"	–5 +/–
	Сообщение от Аноним (-), 18-Июн-17, 21:54
	> Платформа GNU/Hurd не вошла в число официально поддерживаемых архитектур Debian 9, поэтому релиз Debian GNU/Hurd 2017 выпущен отдельно и имеет статус неофициального выпуска Debian В чём разница?
	Ответить | Правка | ^ к родителю #3 | Наверх | Cообщить модератору

	6. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от A.Stahl (ok), 18-Июн-17, 22:18
	Формально ни в чём, а фактически Debian GNU/Hurd долгое время был официальным релизом Debian и когда Hurd подпилят чуток, то снова им станет.
	Ответить | Правка | ^ к родителю #4 | Наверх | Cообщить модератору

	12. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от Аноним (-), 18-Июн-17, 23:04
	> В чём разница? В том, что Debian GNU/Hurd и Debian GNU/KFreeBSD - это _Debian_, а Dyson посторонний продукт, который использует наработки Debian.
	Ответить | Правка | ^ к родителю #4 | Наверх | Cообщить модератору

2. "Увидел свет Debian GNU/Hurd 2017"	+/–
Сообщение от nc (ok), 18-Июн-17, 21:35
А чем это интересно с точки зрения пользователя или даже программиста? Я так понимаю "снаружи" это обычная (может в чем-то урезанная) линуксоподобная система.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	7. "Увидел свет Debian GNU/Hurd 2017"	+8 +/–
	Сообщение от A.Stahl (ok), 18-Июн-17, 22:20
	Ничем. Пока uname не введёшь вообще не поймёшь что ты не в линуксе. И это хорошо.
	Ответить | Правка | ^ к родителю #2 | Наверх | Cообщить модератору

	8. "Увидел свет Debian GNU/Hurd 2017"	+2 +/–
	Сообщение от Аноним (-), 18-Июн-17, 22:25
	Она не может быть линукс-подобной, потому что к линуксовому ядру не имеет ни малейшего отношения. Это HURD, изначальное ядро проекта GNU, на момент 1992 года бывшее в состоянии отсутствия. Потом его очень много раз переписывали с нуля, и вот сейчас оно благополучно заводится. Там мало чего работает, дров почти ни подо что нет, но все-таки это уже полноценный Unix (в отличие от Linux). Кому интересно - в основном, исследователям. Реально работать там сейчас трудно: i386, никаких драйверов кроме совсем generic (типа vesa). Последний раз, когда я ее тыкал, там даже usb не было.
	Ответить | Правка | ^ к родителю #2 | Наверх | Cообщить модератору

	14. "Увидел свет Debian GNU/Hurd 2017"	+3 +/–
	Сообщение от fi (ok), 19-Июн-17, 00:10
	> это уже полноценный Unix соврал не глядя :) - Unix есть торговая марка, есть сертификаты соответствия всякие, типа UNIX 98, за деньги.  Все остальные Unix-like системы в этом смысле не Unix. Во-вторых, сегодня Posix стандарты развивают как lsb, то есть современны Unix системы догоняют Linux - и даже можно говорить о linux-like  :)))))) Ну а сам HURD с i386 и с неудачным mach есть маргинальная система без будущего, увы :(((((
	Ответить | Правка | ^ к родителю #8 | Наверх | Cообщить модератору

	36. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от Аноним (-), 20-Июн-17, 08:50
	>> это уже полноценный Unix > соврал не глядя :) - Unix есть торговая марка, есть сертификаты соответствия > всякие, типа UNIX 98, за деньги.  Все остальные Unix-like системы > в этом смысле не Unix. > Во-вторых, сегодня Posix стандарты развивают как lsb, то есть современны Unix системы > догоняют Linux - и даже можно говорить о linux-like  :)))))) Как-то у вас всё в кучу. Есть развивающийся стандарт POSIX, определяющий понятие Unix-like. Есть платная сертификация, которую нужно пройти, чтобы называться Unix-like «официально». POSIX описывает много всего: списки поддерживаемых команд, API, даже формат некоторых файлов. LSB, определяющий развитие Linux-дистрибутивов, в этой схеме нигде и никак не участвует и развивается параллельно, по большей части дополняя POSIX.
	Ответить | Правка | ^ к родителю #14 | Наверх | Cообщить модератору

	41. "Увидел свет Debian GNU/Hurd 2017"	+/–
	Сообщение от www2 (ok), 21-Июн-17, 17:33
	Но Hurd всё равно никогда не будет Unix'ом, потому что он GNU, что расшифровывается как GNU is Not Unix.
	Ответить | Правка | ^ к родителю #36 | Наверх | Cообщить модератору

	19. "Увидел свет Debian GNU/Hurd 2017"	+4 +/–
	Сообщение от Аноним (-), 19-Июн-17, 09:57
	Драйвера в пространстве пользователя: - можно отлаживать свою ФС от пользователя, не залезая в ядро; - можно использовать свой сетевой стек и настройки сети (например, отдельное приложение или пользователь может работать с VPN, когда все остальное работает напрямую); - и прочее, для чего в Линуксе пришлось бы создавать виртуальную машину (вообще, виртуализация — костыль, в адекватной ОС она будет не нужна).
	Ответить | Правка | ^ к родителю #2 | Наверх | Cообщить модератору

	43. "Увидел свет Debian GNU/Hurd 2017"	–1 +/–
	Сообщение от Аноним (-), 22-Июн-17, 13:07
	> Драйвера в пространстве пользователя: > - можно отлаживать свою ФС от пользователя, не залезая в ядро; > - можно использовать свой сетевой стек и настройки сети (например, отдельное приложение или пользователь может работать с VPN, когда все остальное работает напрямую); > - и прочее, для чего в Линуксе пришлось бы создавать виртуальную машину (вообще, виртуализация — костыль, в адекватной ОС она будет не нужна). Не надо сказок. Все что вы перечислили - все можно сделать без костылей и без просадки в исполнении даже в истинно монолитном (без динамических модулей) ядре. Если вы сомневаетесь, то можете оплатить мою работу и я вам это докажу :)
	Ответить | Правка | ^ к родителю #19 | Наверх | Cообщить модератору

	44. "Увидел свет Debian GNU/Hurd 2017"	–1 +/–
	Сообщение от Аноним (-), 22-Июн-17, 17:30
	Сомневаюсь, оплачивать не буду. Что-то, конечно, можно сделать. Где-то было, например, про реализацию сетевого стека в пространстве пользователя для Линукса, но ведь это уже элемент микроядерной архитектуры и ядро в этом случае уже не совсем монолитное. Вполне возможен и такой вариант развития: Линукс будет со временем приобретать возможности микроядерной ОС и превратится в гибрид.
	Ответить | Правка | ^ к родителю #43 | Наверх | Cообщить модератору

	39. "Увидел свет Debian GNU/Hurd 2017"	–1 +/–
	Сообщение от пох (?), 20-Июн-17, 22:45
	> А чем это интересно с точки зрения пользователя или даже программиста? совершенно ничем (ну, разьве что для общего развития, чтобы понимать, что не все на свете есть линукс - с чем-то более интересным на доступном железе не поиграешь) > Я так понимаю "снаружи" это обычная (может в чем-то урезанная) линуксоподобная система. posix(даже не unix)-подобная. Да. Пока не пытаешься ее сконфигурить хоть как-то под свое железо, ну, или поправить драйвер. Жаль что дебиановские скрипты как раз это все старательно прячут под капотом. Во времена, когда начинать приходилось с "а ну-ка, ну-ка - создай-ка мне fs правильного вендора не имея работающего на твоей системе ядра и юзерленда, а потом кросс-сборкой натяни-ка сову на глобус" было, признаться, поинтереснее. В плане useability оно с тех времен ничуть не продвинулось.
	Ответить | Правка | ^ к родителю #2 | Наверх | Cообщить модератору

13. "Увидел свет Debian GNU/Hurd 2017"	+/–
Сообщение от Аноним (-), 18-Июн-17, 23:30
Чистое микроядро чуток устарело. Да и на mach тормозное выходит. Нужно экзоядро тогда уж, если выбирать хорошее. Но в целом радует, что можно тыкать палкой в GNU/HURD.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	15. "Увидел свет Debian GNU/Hurd 2017"	+/–
	Сообщение от A.Stahl (ok), 19-Июн-17, 06:58
	>Чистое микроядро чуток устарело. И что же такое случилось, что сделало концепцию микроядра устаревшей, хм? Только не надо пальцем тыкать в Линукс. Линукс это как раз то, что поддерживает интерес к микроядрам:)
	Ответить | Правка | ^ к родителю #13 | Наверх | Cообщить модератору

	22. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от Аноним (-), 19-Июн-17, 12:08
	Просто экзоядро это уже следующий этап в развитии микроядер. Там еще более код прост и минимален. Микроядро просто часто, например, обвиняют в низкой производительности по сравнению с монолитными ядрами, например. С экзоядром и эта проблема решается.
	Ответить | Правка | ^ к родителю #15 | Наверх | Cообщить модератору

	20. "Увидел свет Debian GNU/Hurd 2017"	–2 +/–
	Сообщение от Аноним (-), 19-Июн-17, 10:58
	Ну вот DOS была по сути экзоядром. Это же был рай для вирей.
	Ответить | Правка | ^ к родителю #13 | Наверх | Cообщить модератору

	21. "Увидел свет Debian GNU/Hurd 2017"	–3 +/–
	Сообщение от Аноним (-), 19-Июн-17, 12:04
	Там же было монолитное ядро. Экзоядро это не то. Экзоядро бы лишь реализовало некие абстракции типа квант процессорного времени, бит памяти и прочее (это пример, конечно, может и плох, ведь в ЖД всё блоками, ну, в общем, пример), а уже поверх этого строились бы специальные библиотеки. И фактически, экзоядро бы работало над защитой этих ресурсов и несложно управляло ими. Всё остальное над этими квантами и битами (пример опять же для упрощения) в библиотеках уже. Программы используют библиотеки готовые или реализуют свои, но опять же безопасно над этими некоторыми первоначальными собственно вот.
	Ответить | Правка | ^ к родителю #20 | Наверх | Cообщить модератору

	33. "Увидел свет Debian GNU/Hurd 2017"	+/–
	Сообщение от Аноним (-), 20-Июн-17, 01:28
	Отвечу теми же словами: "экзоядро - это не то". Экзоядро никаких абстракций не педоставляет, а лишь по большому счету следит, чтобы процессы друг с другом могли безопасно взаимодействовать. ДОС как раз этим и занимался, пусть и коряво и совершенно неожиданно для самого себя и своих разработчиков.
	Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

	34. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от angra (ok), 20-Июн-17, 03:17
	Нет. Экзоядро оперирует хоть и максимально простыми сущностями(блоки на диске, страницы памяти, кванты процессорного времени), но в enforced режиме, чего в DOS не было и в помине. О каком безопасном взаимодействии может идти речь, если каждой программе были доступны любой участок памяти, блок на диске или весь процессор. Более того, DOS как раз предлагал для программ совсем не примитивные сущности, это делал  BIOS, а довольно продвинутые абстракции, вроде файла на диске. Так что DOS это скорее разделяемая библиотека, но ни одним местом не к экзоядро.
	Ответить | Правка | ^ к родителю #33 | Наверх | Cообщить модератору

	37. "Увидел свет Debian GNU/Hurd 2017"	+/–
	Сообщение от Аноним (-), 20-Июн-17, 08:53
	> Отвечу теми же словами: "экзоядро - это не то". Экзоядро никаких абстракций > не педоставляет, а лишь по большому счету следит, чтобы процессы друг > с другом могли безопасно взаимодействовать. ДОС как раз этим и занимался, > пусть и коряво и совершенно неожиданно для самого себя и своих > разработчиков. Процессы в DOS? Уже смешно. Вы его хоть видели-то, прежде чем говорить такое?
	Ответить | Правка | ^ к родителю #33 | Наверх | Cообщить модератору

	38. "Увидел свет Debian GNU/Hurd 2017"	–4 +/–
	Сообщение от Аноним (-), 20-Июн-17, 20:45
	> Процессы в DOS? Уже смешно. Вы его хоть видели-то, прежде чем говорить такое? Даже в убер-шелле DOS Navigator - были облегчённые-процессы, можно было например копировать файлы и читать что то или писать причём хоть сразу 100 файлов. В некоторых играх под ДОС судя по всему - и обычные потоки были, просто редко, по крайне мере точно видел даже отдельный DOS extender в котором такое заявлялось. В самом (MS)DOS пусть не было потоков "из коробки" - но, многозадачность была! Вполне можно было себе обращаться с сетевой картой параллельно работе её драйвера или звуковушки, т.е.вручную и авоматически ветесняющая многзадачность(посмотрите скольк осейчас пооков в ОС под указанные драйвера) что то типа OVERLAPPED, более того - мало ктознает, но аналогичным методом(OVERLAPPED) - можно было и к диску обращаься! И это втихую использовали разные графические ДОС-шеллы и тем более убер ДОС шеллы от MS'же - начиная с win1.0-3.1 и даже вся линейка win9x сама использовала такие обращения к DOS файловому вводу-вывода [и что осбенно было полезно - даже предосавляя доступ к DOS драйверам диска от третьих производителей, когда под w9x небыло от производителя вообще, например минимум для BIOS-удалённых-дисков, это была ОС с истинной обратная совместимость...]. Просто во времна DOS это было слишком сложно и главное ненужно/неоплачиваемо, тем более при неочевидной пользе при всего 1 ЦПУ, думать о каких о там процессах для линейного однопроцессоного мышления большинства рядовых программистов того времени, ну да да и сама MS - сильно не афишировала конечно все возможности своего клона DOS, оставляя полный функционал только своим же играм и своим шеллам/ОС, а может просто преподам и книгописателям не вмещалсь зачем такой функционал нужен, а раз им не нужно - то и их ученикам...
	Ответить | Правка | ^ к родителю #37 | Наверх | Cообщить модератору

	40. "Увидел свет Debian GNU/Hurd 2017"	+3 +/–
	Сообщение от angra (ok), 21-Июн-17, 00:01
	Вот и стоило писать столько букв только для того, чтобы показать степень своего ламерства?
	Ответить | Правка | ^ к родителю #38 | Наверх | Cообщить модератору

	42. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от www2 (ok), 21-Июн-17, 17:59
	>> Процессы в DOS? Уже смешно. Вы его хоть видели-то, прежде чем говорить такое? > Даже в убер-шелле DOS Navigator - были облегчённые-процессы, можно было например копировать > файлы и читать что то или писать причём хоть сразу 100 > файлов. Вы про DOS вещаете или про навигатор там какой-то? > В некоторых играх под ДОС судя по всему - и обычные потоки > были, просто редко, И каким системным вызовом под DOS можно было создать поток? > по крайне мере точно видел даже отдельный DOS extender в котором такое > заявлялось. DOS extender'ы переводили компьютер в защищённый режим, чтобы им была доступна оперативная память свыше 1 мегабайта без всяких приёмчиков типа оверлеев. Когда программа вызывала программное прерывание, DOS extender переводил на время компьютер в реальный режим, а после возврата из прерывания возвращал обратно в защищённый. > В самом (MS)DOS пусть не было потоков "из коробки" - но, многозадачность > была! Там не было ни процессов, ни потоков. Запустить можно было только одну задачу. Даже запустить из одной задачи другую задачу - было непростой... задачей. Вся виденная вами многозадачность представляла собой функции самой программы - она работала в цикле и вызывала в нём разные функции, которые выполняли разную работу, так что это выглядело как многозадачность. Были ещё резидентные программы, что тоже было только трюком, а не штатной возможностью DOS - резидентные программы перезаписывали адрес в таблице обработчиков прерываний, чтобы какой-то кусок этой программы вызывался при вызове обработчика прерывания, этот кусок потом вызывал тот обработчик, который был записан в таблице обработчиков прерываний до него. Резидентная программа завершалась, прося DOS не удалять себя из памяти. Ещё раз - все эти трюки к DOS отношения не имеют. > Вполне можно было себе обращаться с сетевой картой параллельно работе её драйвера > или звуковушки, т.е.вручную и авоматически ветесняющая многзадачность Вытесняющая многозадачность имеет место тогда, когда операционная система принудительно прерывает выполнение одного процесса, сохраняет его состояние и восстанавливает состояние другого процесса. В DOS процессов не было. Процессы и кооперативная многозадачность были в Windows до появления Windows NT и её потомков - это широко известные версии Windows 3.11, 95, 98 и ME. Вытесняющая многозадачность появилась только в Windows NT и продолжилась в её потомках - Windows 2000, XP и т.д. до нынешних времён. Сеть в DOS была реализована методом резидентных программ. Драйверы сети не были отдельными процессами. >(посмотрите скольк > осейчас пооков в ОС под указанные драйвера) что то типа OVERLAPPED, > более того - мало ктознает, но аналогичным методом(OVERLAPPED) - можно было > и к диску обращаься! Что такое OVERLAPPED и сколько потоков у ОС под "указанные драйвера"? Драйверы в Linux являются модулями ядра и чаще всего не создают отдельных внутриядерных потоков, они просто встраиваются в пространство ядра и могут выполняться даже на нескольких процессорах одновременно, обрабатывая данные от разных устройств параллельно - никаких внутриядерных потоков специально под обработку данных от устройства при этом не создаётся. > И это втихую использовали разные графические ДОС-шеллы и тем более убер ДОС > шеллы от MS'же - начиная с win1.0-3.1 Windows 1.0-3.1 представляли собой программу, которая работает поверх DOS. Windows 1.0-3.1 были надстройками. > и даже вся линейка > win9x сама использовала такие обращения к DOS Windows 95, 98 и ME были самостоятельными операционными системами с DOS'ом как собственной подсистемой. DOS был частью Windows 95, 98 и ME, но не подложкой, поверх которой работала Windows 95, 98 или ME. У этой серии Windows для каждого устройства были собственные драйверы и была кооперативная многозадачность. > файловому вводу-вывода [и что > осбенно было полезно - даже предосавляя доступ к DOS драйверам диска > от третьих производителей, когда под w9x небыло от производителя вообще, например > минимум для BIOS-удалённых-дисков, это была ОС с истинной обратная совместимость...]. В Windows 95, 98 и ME обращения к прерываниям DOS и BIOS перехватывались и обрабатывались самим Windows и её драйверами. > Просто во времна DOS это было слишком сложно и главное ненужно/неоплачиваемо, тем > более при неочевидной пользе при всего 1 ЦПУ, думать о каких > о там процессах для линейного однопроцессоного мышления большинства рядовых программистов > того времени, ну да да и сама MS - сильно не > афишировала конечно все возможности своего клона DOS, оставляя полный функционал только > своим же играм и своим шеллам/ОС, а может просто преподам и > книгописателям не вмещалсь зачем такой функционал нужен, а раз им не > нужно - то и их ученикам... Сейчас есть версии ядра Linux, которое работает на системах без MMU - там есть процессы. Прошивки коммутаторов и маршрутизаторов, сколько помню, всегда представляли собой монолитную прошивку, но и в некоторых из моделей коммутаторов и маршрутизаторов всё равно были процессы. Процессы есть там, где есть хотя бы кооперативная многозадачность. В DOS не было процессов и не было кооперативной многозадачности - DOS была чисто однозадачной системой. Больше не говорите о том, в чём вообще нихрена не понимаете. Тем более так много.
	Ответить | Правка | ^ к родителю #38 | Наверх | Cообщить модератору

	46. "Увидел свет Debian GNU/Hurd 2017"	+/–
	Сообщение от Аноним (46), 03-Май-19, 16:57
	> кооперативная многозадачность > Windows 95/98/Me Бггг. Вытесняющая там была уже, вообще-то. Хотя полностью показать свои преимущества не могла из-за наследия совместимости с DOS. А в остальном плюс-минус правильно.
	Ответить | Правка | ^ к родителю #42 | Наверх | Cообщить модератору

	35. "Увидел свет Debian GNU/Hurd 2017"	+/–
	Сообщение от angra (ok), 20-Июн-17, 03:21
	> Экзоядро бы лишь реализовало некие абстракции типа квант процессорного времени, бит памяти и прочее Бит памяти принципиально не может быть управляемым ресурсом. Но если ты не понимаешь разницу между битом и страницей, то наверное рассуждать об экзоядрах тебе рановато.
	Ответить | Правка | ^ к родителю #21 | Наверх | Cообщить модератору

17. "Увидел свет Debian GNU/Hurd 2017"	–3 +/–
Сообщение от Аноним (-), 19-Июн-17, 08:32
"В новом выпуске ядро GNU Hurd и микроядро GNU Mach обновлены до последних версий 0.9 и 1.3, примечательных заметным повышением стабильности и переработанной системой управления памятью..." Я один идиот или все так считают, что не лучше ли сразу внедрить решение,которое лучше изначального? Придите к общей концепции,господа.
Ответить | Правка | ^ к родителю #0 | Наверх | Cообщить модератору

	18. "Увидел свет Debian GNU/Hurd 2017"	+11 +/–
	Сообщение от A.Stahl (ok), 19-Июн-17, 09:00
	А то понапишут программ с багами вместо того чтобы сразу всё продумать и сделать правильно, да?
	Ответить | Правка | ^ к родителю #17 | Наверх | Cообщить модератору

	23. "Увидел свет Debian GNU/Hurd 2017"	–4 +/–
	Сообщение от Аноним (-), 19-Июн-17, 12:10
	Сразу всё продумать и сделать правильно можно в рамках формальной верификации, например.
	Ответить | Правка | ^ к родителю #18 | Наверх | Cообщить модератору

	24. "Увидел свет Debian GNU/Hurd 2017"	+/–
	Сообщение от A.Stahl (ok), 19-Июн-17, 12:50
	Вот только программисты, ленивые скотины, до сих не придумали методов для универсальной формальной верификации. Ай-яй-яй. Можешь пожурить их.
	Ответить | Правка | ^ к родителю #23 | Наверх | Cообщить модератору

	25. "Увидел свет Debian GNU/Hurd 2017"	–1 +/–
	Сообщение от Аноним (-), 19-Июн-17, 13:02
	Что имеется в виду под универсальной формальной верификацией? Вы там Искусственный Интеллект хотите?
	Ответить | Правка | ^ к родителю #24 | Наверх | Cообщить модератору

	26. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от Andrey Mitrofanov (?), 19-Июн-17, 13:13
	> Что имеется в виду под универсальной формальной верификацией? Вы там Искусственный Интеллект > хотите? Формальная верификация какого-нибудь баша или wget-а не влезет ни в один супер-комп. И вовсе в них тоже не влезет. Кроме того, она [написание её] также не влезет ни в одну голову ни одного человека. Рептилоиды, стройся ЗДЕСя--->>>
	Ответить | Правка | ^ к родителю #25 | Наверх | Cообщить модератору

	27. "Увидел свет Debian GNU/Hurd 2017"	–3 +/–
	Сообщение от Аноним (-), 19-Июн-17, 13:18
	ЧТО, вы в своем уме вообще-то? Всё спокойно влезает, микроядра тоже верифицируют (L4 правда, а не Mach). Сейчас самая продвинутая верификация на системах теории типов, получается весьма компактно и вычислить можно. Тем более, даже здание математики постепенно переносят на теорию типов, правда HoTT (гомотопическая теория типов), что вообще повлечет за собой весомые перемены в математике и даже автоматизацию математиков, если грубо, как бы это не звучало. Стоит изучить вопрос, интересная вещь же.
	Ответить | Правка | ^ к родителю #26 | Наверх | Cообщить модератору

	28. "Увидел свет Debian GNU/Hurd 2017"	+2 +/–
	Сообщение от Andrey Mitrofanov (?), 19-Июн-17, 13:45
	> ЧТО, вы в своем уме вообще-то? Всё спокойно влезает, микроядра тоже верифицируют > (L4 правда, а не Mach). Сейчас самая продвинутая верификация на системах > теории типов, получается весьма компактно и вычислить можно. Тем более, даже > здание математики постепенно переносят на теорию типов, правда HoTT (гомотопическая теория > типов), что вообще повлечет за собой весомые перемены в математике и > даже автоматизацию математиков, если грубо, как бы это не звучало. Стоит > изучить вопрос, интересная вещь же. Изучил. "Formal methods of software development are not widely used in industry. Most companies do not consider it cost-effective to apply them in their software development processes." --https://en.wikipedia.org/wiki/Formal_specification#Limitations "At present, formal verification is used by most or all leading hardware companies, but its use in the software industry is still languishing." --https://en.wikipedia.org/wiki/Formal_verification#Industry_use Ничего интересного. Обычное анонимское враньё и сопли. Хотя, да, я про интель и их успехи после DIV-бага в этом деле наслышан. Ну, хоть кто-то смог, да. Так, что там с верификацией bash-а, wget-а, gcc? Уже Полный Успех, да? Что-то не вижу... + > ЧТО, вы в своем уме вообще-то? >даже здание математики >гомотопическая теория типов Хорошо, что я в чужом уме, а то б и правда повёлся. Ага, щаз.
	Ответить | Правка | ^ к родителю #27 | Наверх | Cообщить модератору

	29. "Увидел свет Debian GNU/Hurd 2017"	–2 +/–
	Сообщение от Аноним (-), 19-Июн-17, 13:53
	Редко используют так редко используют. Много хороших вещей не используют среди широких масс. Вон до людей только недавно дошел Rust с его аффинными типами и все считали это чудом. Может когда-то и формальную верификацию начнут использовать. >Так, что там с верификацией bash-а, wget-а, gcc? Уже Полный Успех, да? Что-то не вижу... А что верифицировать в wget, например? Там же больше вопросов к сетевой подсистеме. Да и в целом bash и gcc полны легаси, переписать на формальную верификацию будет конечно сложно. Но если интересует то да, есть различные формально верифицированные компиляторы, например. >Хорошо, что я в чужом уме, а то б и правда повёлся. Ага, щаз. Хорошая опечатка. Грустно так общаться будто я ссорюсь с вами.
	Ответить | Правка | ^ к родителю #28 | Наверх | Cообщить модератору

	30. "Увидел свет Debian GNU/Hurd 2017"	+1 +/–
	Сообщение от Andrey Mitrofanov (?), 19-Июн-17, 14:08
	> Грустно так общаться будто я ссорюсь с вами. Не грустите. Есть такая несложная возможность не посылать и не "звать" людей туда, куда сам не ходил. И обязательно -- не изображать из себя девочку, услышав ответ. Попробуйте. >>>>>>>Сразу всё продумать и сделать правильно можно в рамках формальной верификации, например.
	Ответить | Правка | ^ к родителю #29 | Наверх | Cообщить модератору

	31. "Увидел свет Debian GNU/Hurd 2017"	+3 +/–
	Сообщение от Аноним84701 (ok), 19-Июн-17, 15:16
	>> bash, wget > ЧТО, вы в своем уме вообще-то? Всё спокойно влезает, микроядра тоже верифицируют > (L4 правда, а не Mach). Вы случайно не интересовались всякими "второстепенными" деталями? https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf > seL4, a third-generation microkernel of L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. А теперь смотрим человеко-часы (точнее, годы): > The overall size 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 (pm) to develop. About 2 person years (py) went into the Haskell prototype (over all project phases), including design, documentation, coding, and testing. > for a total cost of 2.2 py including the Haskell effort. А ведь в wget более 40, а в баше вообще под две сотни тысяч cтрок кода. > Сейчас самая продвинутая верификация на системах > теории типов, получается весьма компактно и вычислить можно. Это все круто, но вы что-то серьезнее приветов миру верифицировать пытались?
	Ответить | Правка | ^ к родителю #27 | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема