История изменений
Исправление SZT, (текущая версия) :
Что-бы найти ошибку в алгоритме, требует искусственный интеллект, который понимает алгоритм на высоком уровне. Поэтому обсуждать эту тему смысла нет.
Нет, там через логики первого порядка и всякие кванторы можно много чего доказать автоматически. А если нельзя - можно использовать естественный человеческий интеллект, а машина может проверять корректность доказательства, которое выдал человек. К тому же вот недавно какой-то ИИ уделал человека в Go так что можно этими задачами доказательства корректности понагружать аппаратуру. И не забывайте про https://ru.wikipedia.org/wiki/Тезис_Чёрча_—_Тьюринга_—_Дойча
Поскольку мозг человека это тоже вполне физическая штука (бредни про душу в расчет не берем), ЭВМ вам должна уметь доказывать все то, что человек может доказать своим органическим мозгом. ЧТД.
Доказывать корректность С++ это нереально. И не нужно.
Реально. Си умеют доказывать, значит и плюсы смогут. А вот насчет нужность - доказательства корректности нужны для особых вещей, например чтобы от переполнения буфера где-нибудь что-нибудь не отказало в самолете или ракете, летящей в небе. Или какой-нибудь автоматики на производстве или АЭС, где цена ошибки слишком высока. Или медицинском оборудовании. Не ваша это ниша просто
Исправление SZT, :
Что-бы найти ошибку в алгоритме, требует искусственный интеллект, который понимает алгоритм на высоком уровне. Поэтому обсуждать эту тему смысла нет.
Нет, там через логики первого порядка и всякие кванторы можно много чего доказать автоматически. А если нельзя - можно использовать естественный человеческий интеллект, а машина может проверять корректность доказательства, которое выдал человек. К тому же вот недавно какой-то ИИ уделал человека в Go так что можно этими задачами доказательства корректности понагружать аппаратуру. И не забывайте про https://ru.wikipedia.org/wiki/Тезис_Чёрча_—_Тьюринга_—_Дойча
Поскольку мозг человека это тоже вполне физическая штука (бредни про душу в расчет не берем), ЭВМ вам должна уметь доказывать все то, что человек может доказать своим органическим мозгом. ЧТД.
Доказывать корректность С++ это нереально. И не нужно.
Реально. Си умеют доказывать, значит и плюсы смогут. А вот насчет нужность - доказательства корректности нужны для особых вещей, например чтобы от переполнения буфера где-нибудь что-нибудь не отказало в самолете или ракете, летящей в небе. Или какой-нибудь автоматики на производстве или АЭС, где цена ошибки слишком высока. Или медицинском оборудовании. Не ваша это ниша просто
Исходная версия SZT, :
Что-бы найти ошибку в алгоритме, требует искусственный интеллект, который понимает алгоритм на высоком уровне. Поэтому обсуждать эту тему смысла нет.
Нет, там через логики первого порядка и всякие кванторы можно много чего доказать автоматически. А если нельзя - можно использовать естественный человеческий интеллект, а машина может проверять корректность доказательства, которое выдал человек. К тому же вот недавно какой-то ИИ уделал человека в Go так что...
Доказывать корректность С++ это нереально. И не нужно.
Реально. Си умеют доказывать, значит и плюсы смогут. А вот насчет нужность - доказательства корректности нужны для особых вещей, например чтобы от переполнения буфера где-нибудь что-нибудь не отказало в самолете или ракете, летящей в небе. Или какой-нибудь автоматики на производстве или АЭС, где цена ошибки слишком высока. Или медицинском оборудовании. Не ваша это ниша просто