AN
Ну раст то херня. Надо помолится ещё и будут фичи все когда ни будь.
Size: a a a
2021 May 03
[
Хм, а главная разница между тайпкласом и интерфейсом в том, что тайпкласс можно реализовать вне объявления структуры?
AN
Допустим ты считал n и m. Проверил что n<m вот. Теперь от n только отнимаешь. Соответственно гарантия остаётся. Может ли такое жидкий хаскель? @zukaboo ? @ anybody ?
H
liquid haskell?
Т8
F*
H
он про haskell спрашивал
AN
Ну.
s
Должен уметь.
Т8
какая гарантия? Типа, отнимать неотрицательное?
AN
Нет. Что неравенство сохраняется.
Т8
так если ты отнимешь отрицательное, то неравенство может нарушиться
AN
Считай что они unsigned
s
Хороший пример с бинарным поиском.
Т8
ну, было бы прикольно. Только как часто стоит такая игра свеч?
AN
Это уже другой вопрос :)
AN
На меня большое впечатление произвела картинка про sel4 ос. Там пруфов на два порядка больше чем кода. Но там они прямо пруфают что она риалтайм гарантии выполняет и так далее. Если пруфать просто выход за границы массива, то наверное не очень сложно.
AN
Кароче я пошел. Если у кого есть тлдр про рефайнмент вс завтипы кидайте. Только эти ваши закарлючки я все равно не пойму))) так что не кидайте.
s
Смотри видео же.
AN
Ааа я думал это просто по приколу. Ок посмотрю 👍