G
спасибо
Size: a a a
2020 March 05
Т8
фантазии, лол
Я не видел на нём проектов. Это какие-то узкие ниши
DS
Т-34 85
Почему нет общепопулярного софта на нём?
Потому что это прувер, софт на нём - это доказательства каких-то утверждений.
На нём CompCert сделали, как пример.
На нём CompCert сделали, как пример.
Т8
Потому что это прувер, софт на нём - это доказательства каких-то утверждений.
На нём CompCert сделали, как пример.
На нём CompCert сделали, как пример.
Вот я и говорю, что это фантазии, что кто-то будет юзать это промышленно
Т8
Для своих сфер - да
DS
Т-34 85
Вот я и говорю, что это фантазии, что кто-то будет юзать это промышленно
Ага, только вот seL4 формально верифицировали на похожей Isabelle, которая по тем же принципам работает.
Т8
Для операционок - вряд ли
Т8
Для игр - нет
Т8
Для биг дейта - не везде
G
Т-34 85
Для операционок - вряд ли
почему?
Т8
И т.д.
G
Т-34 85
Для игр - нет
почему?
λ
Т-34 85
Вот я и говорю, что это фантазии, что кто-то будет юзать это промышленно
как же я люблю отрицателей прогресса
DS
Т-34 85
Для операционок - вряд ли
Вот, seL4 вполне себе верифицировали. А это именно что ОС
λ
у которых мир застыл в статусе кво и они не способны поверить, что в нём может что-то измениться
Т8
почему?
Ну, только если в очень высокоуровневых модулчх
Т8
почему?
Нах оно там нужно?
G
Т-34 85
Ну, только если в очень высокоуровневых модулчх
вопрос остался
DS
Для игр и пользовательского софта оно вряд ли кому-то нужно, с учётом того, как игры пишутся.
А вот для всего остального сгодится ещё как
А вот для всего остального сгодится ещё как
G
Т-34 85
Нах оно там нужно?
чтобы не писать тесты, а писать теоремы (которые ты сам не доказываешь, а с помощью специального софта). тесты пишет человек, они могут быть ошибочными и почти всегда покрывают далеко не все сценарии, теоремы в этом плане выигрывают