П
ну это перевод русский типа :) вообще они шти :)
Оки
Size: a a a
2020 July 19
GN
Но к концу практики у меня на подоконнике был уже свой кустик 😅
Интересная практика.
GN
ну это перевод русский типа :) вообще они шти :)
А чо по фильмам испанским? Снимают чего стоящее?
O
Grey Nomad
Интересная практика.
Ну у меня была маркетинговая практика, а комнату я снимала у художника. В общем, все как в фильмах 😅
AG
по моей, да
AG
баззард недавно наделал шуму в сообществе пруверов своим довольно агрессивным пиаром lean, что даже сподвигло авторов coq добавить режим его эмуляции
AG
он часто зависает в профильном чатике, я с ним даже общался недавно
AG
у нас с ним правда немного области разные, он топит за верификацию классической математики, а я занимаюсь верификацией программ
GN
у нас с ним правда немного области разные, он топит за верификацию классической математики, а я занимаюсь верификацией программ
А оно того стоит? Обычные NotNull верификации на среднем размере проекте убивают IDE.
GN
И это в сильно-типизированном шарпе.
GN
Или вы чистые теоретики?
AG
мы практики, но наша логика встроена не в иде, а в прувер
AG
после верификации в теории можно стереть все логические аннотации и получить чисто императивную программу, но пока этого нет
GN
То есть, вашу тулзу можно запускать в CI ?
GN
Но никак ни в dev-time?
AG
есть разные подходы
AG
например на основе этой логики можно сделать автоматический анализатор типа https://fbinfer.com/
AG
у нас идея в ручном доказательстве корректности, это более надёжно но конечно требует чтобы этим занимался человек, разбирающийся в логике
AG
т.е. там нужно самому выводить инварианты циклов и т.д.