Исходное сообщение
"В ветку ядра Linux-next добавлен код для разработки драйверо..." Отправлено Аноним, 20-Мрт-21 03:40
> В общем случае доказать "корректность" произвольной программы, написанной на тьюринг-полном языке  невозможно. Это доказал Тьюринг в 1936 г. > см. "Проблема остановки" > https://en.wikipedia.org/wiki/Halting_problem 1) В общем случае это верно для машины Тьюринга с _бесконечной_ лентой. Только вот у нас в реальности память - конечная, как бы современные вебпогроммисты не пытались уверить в обратном. > any finite-state machine, if left completely to itself, will fall eventually into a perfectly periodic repetitive pattern. The duration of this repeating pattern cannot exceed the number of internal states of the machine... (Minsky 1967, p. 24) Ну и да, все возможные варианты программ никому, кроме теоретиков, никуда не упали. На практике интересно подмножество, решающее какие-то реальные задачи. 2) > Rust можно считать тьюринг-полным языком, поэтому автоматическое доказательство "корректности" любой программы написанной на Rust невозможно. "нельзя доказать в общем случае => значит нелзя доказать для частного случая" Л-логика.

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:
	Введите код, изображенный на картинке: