r
А как это экспериментально проверить?
Size: a a a
2020 March 05
p
нет, не нужно
Лол
p
r
red75prime
А как это экспериментально проверить?
Может быть любой человек, понимающий монады, посмотрев на диаграммы из теории категорий, скажет "это же очевидно"
DS
ну в таком случае можно комбинировать тесты и доказательства
Нет
λ
red75prime
Может быть любой человек, понимающий монады, посмотрев на диаграммы из теории категорий, скажет "это же очевидно"
не скажет
G
Нет
почему нельзя?
DS
почему нельзя?
Точнее тут сложный вопрос, как их комбинировать и возможно тогда проще разделить приложение на верифицированную библиотеку и потом уже обычное приложение.
DS
Проблема скорее в том, что с текущими технологиями для верифицированной и обычной части придется использовать разные технологии
G
Проблема скорее в том, что с текущими технологиями для верифицированной и обычной части придется использовать разные технологии
Почему? В Frama-C вот можно встраивать теоремы в исходный код тот же
G
чтобы их проверить, просто запускаешь в терминале frama-c -wp -wp-rte <исходники>
DS
Почему? В Frama-C вот можно встраивать теоремы в исходный код тот же
А, на такой штуке, наверное выйдет. Я думал именно речь про ЯП с зависимыми типами, а не про верификацию в целом.
G
А, на такой штуке, наверное выйдет. Я думал именно речь про ЯП с зависимыми типами, а не про верификацию в целом.
там просто рефайнмент типы кастрированные, как бы теоремы к функции = предусловия и постусловия
DS
там просто рефайнмент типы кастрированные, как бы теоремы к функции = предусловия и постусловия
Для такого вроде бы и SMT словеры умеют доказательства генерить, тогда вообще просто.
Т8
первое - "окей, понял", второе - "что, билять?!"
p
К слову про плюсы, мы сегодня слушали трёх дипломников, они в троем пилили проекты на кутэ, сказали что плюсы это заебись, им нравится
λ
Т-34 85
первое - "окей, понял", второе - "что, билять?!"
первое это простое объяснение для тех, кто уже итак знает, второе — мем
G
К слову про плюсы, мы сегодня слушали трёх дипломников, они в троем пилили проекты на кутэ, сказали что плюсы это заебись, им нравится
авторитетный источник 👍
p
авторитетный источник 👍
Один из них мидл, второй Джун, третий на шестом курсе
Для третьего курса это дохуя авторитет
Для третьего курса это дохуя авторитет
λ
К слову про плюсы, мы сегодня слушали трёх дипломников, они в троем пилили проекты на кутэ, сказали что плюсы это заебись, им нравится
вы ещё олимпиадников, которые ничего кроме плюсов в жизни не видели спросили бы