EG
А как ты проверяешь тотальность?
Size: a a a
2020 March 22
AK
Явно (более заметно) видно где ресурс берётся и где освобождается)
Так это скоуп в расте задаёт. Лишняя писанина получится, да и всё.
{
data = mutex.lock();
}
vs
with mutex.lock() as data {
}
Хотя мне по отступам больше второй вариант нравится
{
data = mutex.lock();
}
vs
with mutex.lock() as data {
}
Хотя мне по отступам больше второй вариант нравится
AZ
А как ты проверяешь тотальность?
идрис проверяет тотальность
DS
А как ты проверяешь тотальность?
Ну возьмём агду или идрис, они проверяют
Т8
@Psilon seriously? В первом варианте приходится думать, что там x означает, когда во втором сразу всё понятно - это же просто элемент текущей итерации. Возможно, дело привычки, но синтаксис второго варианта тупо роднее
AZ
в языках типо вейвового для смартконтрактов просто запрещены циклы и рекурсия
EG
Ну возьмём агду или идрис, они проверяют
А это можно сделать в общем случае?
EG
Это ж проблема останова
AZ
А это можно сделать в общем случае?
можно построить такой язык, где это можно проверить
EG
Он будет не Тьюринг-полным
AZ
будет
AZ
часть языка будет ансейф
AZ
которое не проверяется
AZ
и все
EG
Ну, это читерство
AZ
не больше чем раст
AZ
почему борровчекер работает в расте и не работает в плюсах? Потому что язык под это сделан
AZ
Ну, это читерство
или бери вейвовый язык, он не тьюринг полный
DS
Он будет не Тьюринг-полным
Тебе придется для сложных случаев доказывать компилятору вручную факт остановки
AZ
но тотальный и чистый вполне