➔m
Я без стеба, я ж не знаю об этом ничего, я джун
Size: a a a
2021 February 09
➔m
Т.е., действительно не существует подмножества случаев, в котором время, потраченное на это, было бы не оптимальным решением?
Потраченное на написание верификаторов и генераторов
AS
вот именно поэтому люди и пишут верификаторы и генераторы, которые подобный головняк должны снимать с программиста. То есть чтобы для формальной корректности кода надо было прилагать минимум усилий
формальная корректность кода это (сравнительно) простой вопрос, сложнее вопрос как бизнес требования формализовать с помощью кода чтобы верификаторы поймали его нарушение, и пока верификаторы не (сильно) помогают
SZ
Я без стеба, я ж не знаю об этом ничего, я джун
AS
Т.е., действительно не существует подмножества случаев, в котором время, потраченное на это, было бы не оптимальным решением?
существует конечно, в аэроспейсе действительно делают и в медицине
➔m
существует конечно, в аэроспейсе действительно делают и в медицине
Вопрос про другие сферы, там это тоже всегда оптимально?
N
Т.е., действительно не существует подмножества случаев, в котором время, потраченное на это, было бы не оптимальным решением?
в каждом случае надо смотреть. Но смотри - у нас уже может быть логика, описанная в коде, и объекты, которые мы хотим пересылать по сети каким-то образом. Нам бы, очевидно, хотелось, чтобы отправитель и получатель понимали друг друга, поэтому очень удобно описать объекты в виде набора типов, а саму реализацию протокола просто сделать производной из этого описания, через тот же самый генератор, например
AS
Вопрос про другие сферы, там это тоже всегда оптимально?
я не говорил _всегда_ :) но грубо говоря это помогает, например возвращаясь к протоколам - когда ты пишешь FSM для протокола ты его потом можешь формально верифицировать и доказать что он в любых условиях будет работать
N
это не приведет к замедлению работы никак, но иногда повлечет за собой жертвование человекочитаемостью, которая при таком подходе в принципе и не нужна, потому что у нас уже есть формально корректное описание протокола
AS
Вопрос про другие сферы, там это тоже всегда оптимально?
а блин, я запутался в двойных не
AS
нет конечно это не всегда оптимально
➔m
нет конечно это не всегда оптимально
А когда именно это не оптимально?
AS
А когда именно это не оптимально?
по разному, но например когда цена ошибки меньше цены формализации, А х В х С :)
К
Внезапные холода на улице совсем не повод пропускать традиционные завтраки. Разве что встретимся на полчаса позже обычного - просыпаться в такой холод почему-то сложнее. Ждем всех завтра в 9-30 https://www.meetup.com/pybreakfast/events/276245181/?isFirstPublish=true
➔m
по разному, но например когда цена ошибки меньше цены формализации, А х В х С :)
А почему Николай вывел эти кейсы из рассмотрения как вариант опровержения его модели?
N
А когда именно это не оптимально?
кстати, точно так же все это работает с безопасностью данных
AS
А почему Николай вывел эти кейсы из рассмотрения как вариант опровержения его модели?
ну не совсем вывел, он же сказал что сложнее не значит хуже, то есть он просто не согласен с качественной оценкой
AS
извиняюсь за третье лицо
➔m
Я чот вообще не могу догнать про сложнее не значит хуже в данном контексте
AS
Я чот вообще не могу догнать про сложнее не значит хуже в данном контексте
ну типа формальная верификация требует затрат зато потом хорошо работает программа