EG
Ты не можешь в общем случае доказать тотальность для функции Тьюринг-полного языка
Size: a a a
2020 March 22
EG
Либо вводить ансейф, либо отказываться от Тьюринг-полноты
AZ
Ты не можешь в общем случае доказать тотальность для функции Тьюринг-полного языка
тебе не надо общий случай, тебе надо частный
DS
Ты не можешь в общем случае доказать тотальность для функции Тьюринг-полного языка
Да, тогда придется переписывать программу так, чтобы это можно было доказать.
EG
То есть Алекс предлагает отказаться от тотальности, а Доге от Тьюринг-полноты
DS
Но это языки с зависимыми типами, там всегда так
Т8
почему борровчекер работает в расте и не работает в плюсах? Потому что язык под это сделан
как же тогда работают анализаторы PVS и Clang?
DS
То есть Алекс предлагает отказаться от тотальности, а Доге от Тьюринг-полноты
Да, Тьюринг полнота переоценена в какой-то мере
AZ
Т-34 85
как же тогда работают анализаторы PVS и Clang?
1) они дают ложные срабатывания
2) кучу всего они не ловят
2) кучу всего они не ловят
AZ
а они работаю на эвристиках, известно же
AZ
"если тут у нас есть указатель то посмотрим, не проверяют ли там дальше на нулл"
AZ
"проверяют. ну, наверное всё ок"
Т8
1) они дают ложные срабатывания
2) кучу всего они не ловят
2) кучу всего они не ловят
как будто борров чекер не режет тогда, когда можно допустить данный код
Т8
когда ничего страшного не случится
EG
Да, Тьюринг полнота переоценена в какой-то мере
Кажется, что тогда много чего разумного написать не выйдет
Т8
Кажется, что тогда много чего разумного написать не выйдет
+
AZ
Кажется, что тогда много чего разумного написать не выйдет
почему-то ты считаешь что тьюринг-неполный означает "игрушечный для конкретной задачи"
EG
Не знаю ни одного не Тьюринг-полного языка, который хоть кто-то использует
DS
Не знаю ни одного не Тьюринг-полного языка, который хоть кто-то использует
Любой язык с зависимыми типами, считай.
Там везде есть ансейфы, но твои доказательства всегда не полные по Тьюрингу
Там везде есть ансейфы, но твои доказательства всегда не полные по Тьюрингу
EG
Только совсем уж локальные DSL