Тем временем подавляющее число разработчиков: - Я не знаю как это работает, оно не ломается и ладно

@user-pn8fo3zq8o

2 жыл бұрын

Ну не знаю... Последние лет пять скорее "я знаю, как оно работает, и слава Богу что я не ошибся". А потом оказывается, что ошибся)))

Я понимаю что на простой задаче это можно классно расписать, но на реальной задаче я не представляю как это можно использовать. Мне всегда казалось что формальное представление программ (алгоритмов) это конечно хорошо, но дальше университета на практике вообще не применимо, ибо подобная запись сильно далека от простого человеческого понятия и никто на практике таким заниматься не будет. Было бы замечательно увидеть пример анализа на небольшом проекте :)

@user-ps6bb1fm9u

2 жыл бұрын

Проблема всех этих видео, со всеми этими методами - сейчас я вам покажу как эффективно делать %some% на примере hello world. А дальше hello world это конечно же работает, возможно формально описать (наверное возможно, опять же мои познания в этом небольшие) задачу, алгоритм и т.д., но в чем я уверен, так это в том, что любую реальную задачу из реально бизнеса, невероятно сложно формализовать и потребуется x3 если не больше времени на разработку, которую никто вам никогда не даст, ради того, чтобы вы там свои математические штучки расписывали. Это возможно разве, что на очень серьезных проектах, авиация, ПО для систем реального времени, реакторы там ядерные и т.д. и т.п. А в задачах даже серьезного софта энтерпрайз уровня вам врятли удастся выделить столько времени на верификацию ПО.

@VasjaG

Жыл бұрын

Если сделать пример из реальной жизни, то вам придётся потратить МНОГО мозговых усилий, чтобы это понять. Поэтому зрители такого контента просто не станут это смотреть. +так будет труднее применить эти знания уже в своём проекте. поэтому проще показать простой пример, а дальше уже всё зависит от вашей смекалки. Это не говоря, про авторские права на реальный пример. (есть пример, когда очень ценного сотрудника уволили за то, что на полузакрытой конференции в общей форме рассказал пример с работы)

Правильно! Так их! Наимпортируют библиотек всяких в питонах своих и давай абстракцию реализовывать, да код со стаковерфлоу адаптировать! То ли дело мы - настоящие погромисты, пару циклов написал - рабочий день закончился. Зато без багов.

Одна проблема. Как это все успеть сделать между срочной и очень срочной задачами)

Спасибо за видео, но не понимаю как показанное вами можно применить к реальному коду решающему бизнес задачу, буду благодарен если в одном из следующих видео это продемонстрируете. А ещё поделитесь, пожалуйста, литературой или сайтами где в подобное можно углубиться новичку.

По большому счету вопрос типизации в рамках решаемой задачи является изучение (представление) изменения переменной в граничных условиях, а время разработки и качество кода будет определяться тем насколько хорошо программист (ка) будет знать эти граничные условия

Евгений, хотелось бы конечно увидеть подобного рода верификацию не формальных вещей, типа математики и типов данных, а неформальных - бизнес правил. Как можно построить мат. модель реальной предметной области, где не то что формализмом, иногда даже здравым смыслом не пахнет. "Выдавать скидку каждому 4 клиенту в 10 день после последнего полнолуния, с условием, что у клиента среди приведенных им в наш сервис пользователей есть его родственник мужского пола по имени Зина."

@goosedb4470

2 жыл бұрын

Для тебя, видимо, верификация работает каким-то магическим образом. Для того, чтобы доказать некоторые свойства программы, нужно задать аксиомы, исходя из которых можно доказать некоторые теоремы. Какие аксиомы у тебя в твоей _бизнес логике_?

@user-ps6bb1fm9u

2 жыл бұрын

@@goosedb4470 Спасибо большое, я понимаю, что нужно сделать для верификакации, но в том и вопрос: как определить аксиомы для реальных приложений, не игрушечных, не учебных, где предметная область сама по себе не имеет четкой формализации и очень часто в которой размытые понятия. Евгений показал нам способ как верифицировать корректность ПО, где можно довольно просто определить аксиомы, где все базируется на просто школьной математике и используются её аксиомы. Т.е. предметная область приложения показанного в видео, это инкрементирование чисел, т.е. сложение, т.е. правила предметной области в целом совпадают с правилами математики. "Какие аксиомы у тебя в твоей _бизнес логике_?". В том то и дело, если бы в реальных приложениях которые пишутся для удовлетворения потребностей реального бизнеса были бы аксиомы, то моего вопроса бы не было.

@goosedb4470

2 жыл бұрын

@@user-ps6bb1fm9u ну вот и не может быть формальной верификации без аксиом

@user-ps6bb1fm9u

2 жыл бұрын

@@goosedb4470 ну то есть метод показанный Евгением в коммерческой разработке обычных приложений, которые пишут обычные программисты - не применим.

@S0ERDEVS

2 жыл бұрын

Ответил в своем телеграм канале - t.me/softwareengineervlog/887

Спасибо Женя)

Спасибо!

оооочень сложно но все таки допер. для тех кто не понял приведу более простую аналогию. чтобы выполнилось условие i>=0 марио должен идти по правой части экрана, но в случае когда i=-1 марио идет в левую часть экрана и появляется с правой части, что не попадает под условие (с точки зрения математики получается 0-1=n, где n это максимум) потому и возникает рекурсия, а i=-1 возникает как раз из-за математической коллизии)

Привет Соер) Я баги убираю с помощью отладчика. Ну и обработки try catch. В край отлаживаю в ASM с помощью гидры, ида про, и x64dbg

Про Isabelle/HOL, Coq, Lean не планируете видео?

Спасибо за видео! Метод достаточно интересен, но на практике в большинстве бизнесовых задач не особо вижу применение в связи с высокой степенью волокиты с анализом и формализацией алгоритма. Зачастую также приходится полагаться на объекты, то есть на структуры данных местами крупные и такой анализ кропотливый просто с точки зрения время затрат по мне неособо оправдан в day to day work. Думаю оттачивание практики написания тестов и достижения ими хорошего покрытия (path coverage, например), а также навык поиска и определения так называемых "edge cases" может помочь. Также можно посмотреть в сторону мутационного тестирования кода, которое тоже может хорошо выявить различного рода потенциальные бажки в критически важных для продукта местах.

@pavelnemchenko8570

2 жыл бұрын

Возможно, качественный стат. анализ кода также поможет избежать потенциальных багов и поможет найти граничные знач-я для тестов )

Воу, компьютерная графика очень даже приятная :)

TLDR: Не ешь суп ножом.

@dann1kid

2 жыл бұрын

спасибо

Не могу понять, а как вы поднимаетесь с кейса бомжа? я пробовал пару раз и чето не пошло

А может быть просто стоило бы убрать это так называемое кольцо из языков программирования, чтобы компилятор сразу ошибку выдавал. Или для чего оно нужно уж тогда?

Сложновато, а значит нецелесообразно, ну в областях атомной энергетики , космонавтики и военной техники вполне реальный подход))

👍👍👍👍

Спасибо, очень лаконично и познавательно

11:58. Представляем типы как множество... О каких типах идет речь? О числовых и символьных? Это понятно. Структура и класс - это вроде тоже типы. Их как будем приводить к множеству и диапазону?

@IvanIvanov-wn7ep

2 жыл бұрын

Тип определяется множеством значений, который объект может принимать, множеством операций, которые можно над ним производить и для объектов классов - множеством интерфейсов, к которым можно обращаться.

@AlexAlex-ms3bg

2 жыл бұрын

@@IvanIvanov-wn7ep Это понятно. Но вопрос был о другом - "как"

@IvanIvanov-wn7ep

2 жыл бұрын

​@@AlexAlex-ms3bg я же говорю, что придётся рассматривать все множества свойств объекта: множество возможных значений, множество операций и множество интерфейсов. Если с числовыми понятно как, то что здесь непонятно? Проверять на возможность ошибок не только в плане принимаемых значений, но и в плане операций (подходит та или иная операция для объекта) и в плане интерфейсов (правильно ли объект используется другими объектами)

Как называется тема для KDE? Извиняюсь за оффтоп.

не очень понятно вот что. мы потратили 5 минут на формализацию 1 переменной и цикла с ней. в идеале у нас должна вся программа быть описана математически, так? то есть это этап проектирования, который должен быть у любого хорошего софта? во сколько раз это замедляет разработку?

@IvanIvanov-wn7ep

2 жыл бұрын

Ускоряет, так как экономит время на вылов багов в последствии)

@user-yw2xc2kc6p

Жыл бұрын

​@@IvanIvanov-wn7ep важнее выпустить продукт быстрее, чтобы быстрее охватить рынок, а уже потом заниматься рефактором

А как искать баги, связанные с многопоточностью?

Здравствуйте, подскажите пожалуйста не могли бы Вы помочь в проблеме с кодом пожалуйста

ничего не понятно, но очень интересно 😁

Оккама достаёт свою бритву

Это намек, что надо переходить на haskell ?

@kotikvacia9970

2 жыл бұрын

В чат зашел один Брагилевский

Спасибо за видео, но людям нужно немного другое. Тем кто не знает о статических анализаторах, нужны не только основы теории, а названия конкретных инструментов и описание того, что они могут. Тем, же кто знает о них (они наверное подумали, "ясен пень тут всегда истинное условие, мой анализатор такие варнинги пачками выдает") нужны не основы теории, а либо рецепт решения их проблем, таких как проблема десяти тысяч варнингов, или проблема мегабайт говнокода, либо продвинутая теория, которая объяснит можно ли это применить на высоких слоях абстракции. В общем кликбейтное бесполезное видео.

Было бы очень интересно послушать о том сколько ты зарабатываешь , сколько имеешь свободного времени, и про приоритеты - за какие бы деньги минимум согласился работать на неинтересной (но очень высокооплачиваемой) работе и за какие деньги минимум согласился бы работать на сверхинтересной (по твоему вкусу) работе.

После 10 минуты я понял что теряю время . Описанные ошибки возникают из-за того что программист не владеет языком ( и скорее всего головой) . Любая книга по языку до 2005 года начиналась с изучения типов и изучения поведения типов в подобных ситуациях , чтобы сразу дать пирожок с полки для ума , где может быть засада . Подобные ошибки я допускал где-то в первые год-два, по неопытности и 15 летнему возрасту , но не по незнанию мат части, просто тогда я ещё не допетрил до момента логирования. Проводить тесты на такие ошибки бессмысленно , надо искать грамотных людей владеющих языком , а не вот это вот всё. Даже с точки зрения бюджета это на порядок выгоднее .

а я думал, что если из 0 вычесть единицу, то программа упадет. Пойду посмотрю что будет, если так сделать в Java, думаю что IllegalArgumentException будет.

никто из рядовых разрабов(а именно они локомотивы бОльшей части кода) этим заниматься не будет, да и сеньеры тоже, только скорее увлеченные. Ты предлагаешь забивать мебельные гвоздики огромной кувалдой - это не решение проблемы. Ты затронул решение по типам, только как по мне ушел не в ту степь. На самом деле на уровне типа должно выражение 0 - 1 завершать программу с ошибкой. Для человека механизм переполнения не естественный, потому стоит его обрабатывать явно (явное лучше неявного). В твоем примере ошибка была допущена аж на этапе дизайна языка. Например rust требует такое поведение описать явно, когда ты делаешь математические операции. Хороший пример, показательный, почему люди е любят C/C++. На ровном месте отстрелил себе колено :)

@snatvb

2 жыл бұрын

PS вместо того чтоб бороться с человеческой природой, возможно стоит делать языки и инструменты более интуитивно понятные и ориентированные человеку(в целом тенденция сейчас такая и есть). Дизайн это и делает, так и появился UI.

Вы переехали в страну с легализированными наркотиками?

Кто-то ещё утверждает, что математика программистам не нужна?

27 минут воды. В итоге баг так и не исправил. Очень мощный метод.

@nmg_prm

2 жыл бұрын

Тема не об исправлении, а о методах поиска

@IvanIvanov-wn7ep

2 жыл бұрын

@Anton Shvedov принтф как раз запутал и ничего не показал в чём состоит баг.