Я понимаю что на простой задаче это можно классно расписать, но на реальной задаче я не представляю как это можно использовать. Мне всегда казалось что формальное представление программ (алгоритмов) это конечно хорошо, но дальше университета на практике вообще не применимо, ибо подобная запись сильно далека от простого человеческого понятия и никто на практике таким заниматься не будет. Было бы замечательно увидеть пример анализа на небольшом проекте :)
Проблема всех этих видео, со всеми этими методами - сейчас я вам покажу как эффективно делать %some% на примере hello world. А дальше hello world это конечно же работает, возможно формально описать (наверное возможно, опять же мои познания в этом небольшие) задачу, алгоритм и т.д., но в чем я уверен, так это в том, что любую реальную задачу из реально бизнеса, невероятно сложно формализовать и потребуется x3 если не больше времени на разработку, которую никто вам никогда не даст, ради того, чтобы вы там свои математические штучки расписывали. Это возможно разве, что на очень серьезных проектах, авиация, ПО для систем реального времени, реакторы там ядерные и т.д. и т.п. А в задачах даже серьезного софта энтерпрайз уровня вам врятли удастся выделить столько времени на верификацию ПО.
Если сделать пример из реальной жизни, то вам придётся потратить МНОГО мозговых усилий, чтобы это понять. Поэтому зрители такого контента просто не станут это смотреть. +так будет труднее применить эти знания уже в своём проекте. поэтому проще показать простой пример, а дальше уже всё зависит от вашей смекалки. Это не говоря, про авторские права на реальный пример. (есть пример, когда очень ценного сотрудника уволили за то, что на полузакрытой конференции в общей форме рассказал пример с работы)
Правильно! Так их! Наимпортируют библиотек всяких в питонах своих и давай абстракцию реализовывать, да код со стаковерфлоу адаптировать! То ли дело мы - настоящие погромисты, пару циклов написал - рабочий день закончился. Зато без багов.
Спасибо за видео, но не понимаю как показанное вами можно применить к реальному коду решающему бизнес задачу, буду благодарен если в одном из следующих видео это продемонстрируете. А ещё поделитесь, пожалуйста, литературой или сайтами где в подобное можно углубиться новичку.
По большому счету вопрос типизации в рамках решаемой задачи является изучение (представление) изменения переменной в граничных условиях, а время разработки и качество кода будет определяться тем насколько хорошо программист (ка) будет знать эти граничные условия
Евгений, хотелось бы конечно увидеть подобного рода верификацию не формальных вещей, типа математики и типов данных, а неформальных - бизнес правил. Как можно построить мат. модель реальной предметной области, где не то что формализмом, иногда даже здравым смыслом не пахнет. "Выдавать скидку каждому 4 клиенту в 10 день после последнего полнолуния, с условием, что у клиента среди приведенных им в наш сервис пользователей есть его родственник мужского пола по имени Зина."
Для тебя, видимо, верификация работает каким-то магическим образом. Для того, чтобы доказать некоторые свойства программы, нужно задать аксиомы, исходя из которых можно доказать некоторые теоремы. Какие аксиомы у тебя в твоей _бизнес логике_?
@@goosedb4470 Спасибо большое, я понимаю, что нужно сделать для верификакации, но в том и вопрос: как определить аксиомы для реальных приложений, не игрушечных, не учебных, где предметная область сама по себе не имеет четкой формализации и очень часто в которой размытые понятия. Евгений показал нам способ как верифицировать корректность ПО, где можно довольно просто определить аксиомы, где все базируется на просто школьной математике и используются её аксиомы. Т.е. предметная область приложения показанного в видео, это инкрементирование чисел, т.е. сложение, т.е. правила предметной области в целом совпадают с правилами математики. "Какие аксиомы у тебя в твоей _бизнес логике_?". В том то и дело, если бы в реальных приложениях которые пишутся для удовлетворения потребностей реального бизнеса были бы аксиомы, то моего вопроса бы не было.
оооочень сложно но все таки допер. для тех кто не понял приведу более простую аналогию. чтобы выполнилось условие i>=0 марио должен идти по правой части экрана, но в случае когда i=-1 марио идет в левую часть экрана и появляется с правой части, что не попадает под условие (с точки зрения математики получается 0-1=n, где n это максимум) потому и возникает рекурсия, а i=-1 возникает как раз из-за математической коллизии)
Спасибо за видео! Метод достаточно интересен, но на практике в большинстве бизнесовых задач не особо вижу применение в связи с высокой степенью волокиты с анализом и формализацией алгоритма. Зачастую также приходится полагаться на объекты, то есть на структуры данных местами крупные и такой анализ кропотливый просто с точки зрения время затрат по мне неособо оправдан в day to day work. Думаю оттачивание практики написания тестов и достижения ими хорошего покрытия (path coverage, например), а также навык поиска и определения так называемых "edge cases" может помочь. Также можно посмотреть в сторону мутационного тестирования кода, которое тоже может хорошо выявить различного рода потенциальные бажки в критически важных для продукта местах.
не очень понятно вот что. мы потратили 5 минут на формализацию 1 переменной и цикла с ней. в идеале у нас должна вся программа быть описана математически, так? то есть это этап проектирования, который должен быть у любого хорошего софта? во сколько раз это замедляет разработку?
11:58. Представляем типы как множество... О каких типах идет речь? О числовых и символьных? Это понятно. Структура и класс - это вроде тоже типы. Их как будем приводить к множеству и диапазону?
Тип определяется множеством значений, который объект может принимать, множеством операций, которые можно над ним производить и для объектов классов - множеством интерфейсов, к которым можно обращаться.
@@AlexAlex-ms3bg я же говорю, что придётся рассматривать все множества свойств объекта: множество возможных значений, множество операций и множество интерфейсов. Если с числовыми понятно как, то что здесь непонятно? Проверять на возможность ошибок не только в плане принимаемых значений, но и в плане операций (подходит та или иная операция для объекта) и в плане интерфейсов (правильно ли объект используется другими объектами)
Было бы очень интересно послушать о том сколько ты зарабатываешь , сколько имеешь свободного времени, и про приоритеты - за какие бы деньги минимум согласился работать на неинтересной (но очень высокооплачиваемой) работе и за какие деньги минимум согласился бы работать на сверхинтересной (по твоему вкусу) работе.
А может быть просто стоило бы убрать это так называемое кольцо из языков программирования, чтобы компилятор сразу ошибку выдавал. Или для чего оно нужно уж тогда?
никто из рядовых разрабов(а именно они локомотивы бОльшей части кода) этим заниматься не будет, да и сеньеры тоже, только скорее увлеченные. Ты предлагаешь забивать мебельные гвоздики огромной кувалдой - это не решение проблемы. Ты затронул решение по типам, только как по мне ушел не в ту степь. На самом деле на уровне типа должно выражение 0 - 1 завершать программу с ошибкой. Для человека механизм переполнения не естественный, потому стоит его обрабатывать явно (явное лучше неявного). В твоем примере ошибка была допущена аж на этапе дизайна языка. Например rust требует такое поведение описать явно, когда ты делаешь математические операции. Хороший пример, показательный, почему люди е любят C/C++. На ровном месте отстрелил себе колено :)
PS вместо того чтоб бороться с человеческой природой, возможно стоит делать языки и инструменты более интуитивно понятные и ориентированные человеку(в целом тенденция сейчас такая и есть). Дизайн это и делает, так и появился UI.
После 10 минуты я понял что теряю время . Описанные ошибки возникают из-за того что программист не владеет языком ( и скорее всего головой) . Любая книга по языку до 2005 года начиналась с изучения типов и изучения поведения типов в подобных ситуациях , чтобы сразу дать пирожок с полки для ума , где может быть засада . Подобные ошибки я допускал где-то в первые год-два, по неопытности и 15 летнему возрасту , но не по незнанию мат части, просто тогда я ещё не допетрил до момента логирования. Проводить тесты на такие ошибки бессмысленно , надо искать грамотных людей владеющих языком , а не вот это вот всё. Даже с точки зрения бюджета это на порядок выгоднее .
а я думал, что если из 0 вычесть единицу, то программа упадет. Пойду посмотрю что будет, если так сделать в Java, думаю что IllegalArgumentException будет.
Тем временем подавляющее число разработчиков:
- Я не знаю как это работает, оно не ломается и ладно
Ну не знаю... Последние лет пять скорее "я знаю, как оно работает, и слава Богу что я не ошибся". А потом оказывается, что ошибся)))
Я понимаю что на простой задаче это можно классно расписать, но на реальной задаче я не представляю как это можно использовать. Мне всегда казалось что формальное представление программ (алгоритмов) это конечно хорошо, но дальше университета на практике вообще не применимо, ибо подобная запись сильно далека от простого человеческого понятия и никто на практике таким заниматься не будет. Было бы замечательно увидеть пример анализа на небольшом проекте :)
Проблема всех этих видео, со всеми этими методами - сейчас я вам покажу как эффективно делать %some% на примере hello world. А дальше hello world это конечно же работает, возможно формально описать (наверное возможно, опять же мои познания в этом небольшие) задачу, алгоритм и т.д., но в чем я уверен, так это в том, что любую реальную задачу из реально бизнеса, невероятно сложно формализовать и потребуется x3 если не больше времени на разработку, которую никто вам никогда не даст, ради того, чтобы вы там свои математические штучки расписывали. Это возможно разве, что на очень серьезных проектах, авиация, ПО для систем реального времени, реакторы там ядерные и т.д. и т.п. А в задачах даже серьезного софта энтерпрайз уровня вам врятли удастся выделить столько времени на верификацию ПО.
Если сделать пример из реальной жизни, то вам придётся потратить МНОГО мозговых усилий, чтобы это понять. Поэтому зрители такого контента просто не станут это смотреть. +так будет труднее применить эти знания уже в своём проекте. поэтому проще показать простой пример, а дальше уже всё зависит от вашей смекалки.
Это не говоря, про авторские права на реальный пример. (есть пример, когда очень ценного сотрудника уволили за то, что на полузакрытой конференции в общей форме рассказал пример с работы)
Правильно! Так их! Наимпортируют библиотек всяких в питонах своих и давай абстракцию реализовывать, да код со стаковерфлоу адаптировать!
То ли дело мы - настоящие погромисты, пару циклов написал - рабочий день закончился. Зато без багов.
Спасибо за видео, но не понимаю как показанное вами можно применить к реальному коду решающему бизнес задачу, буду благодарен если в одном из следующих видео это продемонстрируете. А ещё поделитесь, пожалуйста, литературой или сайтами где в подобное можно углубиться новичку.
По большому счету вопрос типизации в рамках решаемой задачи является изучение (представление) изменения переменной в граничных условиях, а время разработки и качество кода будет определяться тем насколько хорошо программист (ка) будет знать эти граничные условия
Одна проблема. Как это все успеть сделать между срочной и очень срочной задачами)
Евгений, хотелось бы конечно увидеть подобного рода верификацию не формальных вещей, типа математики и типов данных, а неформальных - бизнес правил. Как можно построить мат. модель реальной предметной области, где не то что формализмом, иногда даже здравым смыслом не пахнет. "Выдавать скидку каждому 4 клиенту в 10 день после последнего полнолуния, с условием, что у клиента среди приведенных им в наш сервис пользователей есть его родственник мужского пола по имени Зина."
Для тебя, видимо, верификация работает каким-то магическим образом.
Для того, чтобы доказать некоторые свойства программы, нужно задать аксиомы, исходя из которых можно доказать некоторые теоремы. Какие аксиомы у тебя в твоей _бизнес логике_?
@@goosedb4470 Спасибо большое, я понимаю, что нужно сделать для верификакации, но в том и вопрос: как определить аксиомы для реальных приложений, не игрушечных, не учебных, где предметная область сама по себе не имеет четкой формализации и очень часто в которой размытые понятия. Евгений показал нам способ как верифицировать корректность ПО, где можно довольно просто определить аксиомы, где все базируется на просто школьной математике и используются её аксиомы. Т.е. предметная область приложения показанного в видео, это инкрементирование чисел, т.е. сложение, т.е. правила предметной области в целом совпадают с правилами математики.
"Какие аксиомы у тебя в твоей _бизнес логике_?". В том то и дело, если бы в реальных приложениях которые пишутся для удовлетворения потребностей реального бизнеса были бы аксиомы, то моего вопроса бы не было.
@@ДенисДавыдов-ц6х ну вот и не может быть формальной верификации без аксиом
@@goosedb4470 ну то есть метод показанный Евгением в коммерческой разработке обычных приложений, которые пишут обычные программисты - не применим.
Ответил в своем телеграм канале - t.me/softwareengineervlog/887
оооочень сложно но все таки допер. для тех кто не понял приведу более простую аналогию. чтобы выполнилось условие i>=0 марио должен идти по правой части экрана, но в случае когда i=-1 марио идет в левую часть экрана и появляется с правой части, что не попадает под условие (с точки зрения математики получается 0-1=n, где n это максимум) потому и возникает рекурсия, а i=-1 возникает как раз из-за математической коллизии)
Спасибо за видео! Метод достаточно интересен, но на практике в большинстве бизнесовых задач не особо вижу применение в связи с высокой степенью волокиты с анализом и формализацией алгоритма. Зачастую также приходится полагаться на объекты, то есть на структуры данных местами крупные и такой анализ кропотливый просто с точки зрения время затрат по мне неособо оправдан в day to day work. Думаю оттачивание практики написания тестов и достижения ими хорошего покрытия (path coverage, например), а также навык поиска и определения так называемых "edge cases" может помочь. Также можно посмотреть в сторону мутационного тестирования кода, которое тоже может хорошо выявить различного рода потенциальные бажки в критически важных для продукта местах.
Возможно, качественный стат. анализ кода также поможет избежать потенциальных багов и поможет найти граничные знач-я для тестов )
Про Isabelle/HOL, Coq, Lean не планируете видео?
не очень понятно вот что. мы потратили 5 минут на формализацию 1 переменной и цикла с ней. в идеале у нас должна вся программа быть описана математически, так? то есть это этап проектирования, который должен быть у любого хорошего софта? во сколько раз это замедляет разработку?
Ускоряет, так как экономит время на вылов багов в последствии)
@@IvanIvanov-wn7ep важнее выпустить продукт быстрее, чтобы быстрее охватить рынок, а уже потом заниматься рефактором
11:58. Представляем типы как множество... О каких типах идет речь? О числовых и символьных? Это понятно. Структура и класс - это вроде тоже типы. Их как будем приводить к множеству и диапазону?
Тип определяется множеством значений, который объект может принимать, множеством операций, которые можно над ним производить и для объектов классов - множеством интерфейсов, к которым можно обращаться.
@@IvanIvanov-wn7ep Это понятно. Но вопрос был о другом - "как"
@@AlexAlex-ms3bg я же говорю, что придётся рассматривать все множества свойств объекта: множество возможных значений, множество операций и множество интерфейсов.
Если с числовыми понятно как, то что здесь непонятно?
Проверять на возможность ошибок не только в плане принимаемых значений, но и в плане операций (подходит та или иная операция для объекта) и в плане интерфейсов (правильно ли объект используется другими объектами)
Спасибо Женя)
Было бы очень интересно послушать о том сколько ты зарабатываешь , сколько имеешь свободного времени, и про приоритеты - за какие бы деньги минимум согласился работать на неинтересной (но очень высокооплачиваемой) работе и за какие деньги минимум согласился бы работать на сверхинтересной (по твоему вкусу) работе.
А может быть просто стоило бы убрать это так называемое кольцо из языков программирования, чтобы компилятор сразу ошибку выдавал. Или для чего оно нужно уж тогда?
Воу, компьютерная графика очень даже приятная :)
Не могу понять, а как вы поднимаетесь с кейса бомжа? я пробовал пару раз и чето не пошло
TLDR: Не ешь суп ножом.
спасибо
Сложновато, а значит нецелесообразно, ну в областях атомной энергетики , космонавтики и военной техники вполне реальный подход))
👍👍👍👍
Спасибо!
Здравствуйте, подскажите пожалуйста не могли бы Вы помочь в проблеме с кодом пожалуйста
Спасибо, очень лаконично и познавательно
Это намек, что надо переходить на haskell ?
В чат зашел один Брагилевский
никто из рядовых разрабов(а именно они локомотивы бОльшей части кода) этим заниматься не будет, да и сеньеры тоже, только скорее увлеченные. Ты предлагаешь забивать мебельные гвоздики огромной кувалдой - это не решение проблемы. Ты затронул решение по типам, только как по мне ушел не в ту степь. На самом деле на уровне типа должно выражение 0 - 1 завершать программу с ошибкой. Для человека механизм переполнения не естественный, потому стоит его обрабатывать явно (явное лучше неявного). В твоем примере ошибка была допущена аж на этапе дизайна языка. Например rust требует такое поведение описать явно, когда ты делаешь математические операции. Хороший пример, показательный, почему люди е любят C/C++. На ровном месте отстрелил себе колено :)
PS вместо того чтоб бороться с человеческой природой, возможно стоит делать языки и инструменты более интуитивно понятные и ориентированные человеку(в целом тенденция сейчас такая и есть). Дизайн это и делает, так и появился UI.
После 10 минуты я понял что теряю время . Описанные ошибки возникают из-за того что программист не владеет языком ( и скорее всего головой) . Любая книга по языку до 2005 года начиналась с изучения типов и изучения поведения типов в подобных ситуациях , чтобы сразу дать пирожок с полки для ума , где может быть засада . Подобные ошибки я допускал где-то в первые год-два, по неопытности и 15 летнему возрасту , но не по незнанию мат части, просто тогда я ещё не допетрил до момента логирования. Проводить тесты на такие ошибки бессмысленно , надо искать грамотных людей владеющих языком , а не вот это вот всё. Даже с точки зрения бюджета это на порядок выгоднее .
А как искать баги, связанные с многопоточностью?
ничего не понятно, но очень интересно 😁
Оккама достаёт свою бритву
Как называется тема для KDE? Извиняюсь за оффтоп.
а я думал, что если из 0 вычесть единицу, то программа упадет. Пойду посмотрю что будет, если так сделать в Java, думаю что IllegalArgumentException будет.
Кто-то ещё утверждает, что математика программистам не нужна?
Вы переехали в страну с легализированными наркотиками?
27 минут воды. В итоге баг так и не исправил. Очень мощный метод.
Тема не об исправлении, а о методах поиска
@Anton Shvedov принтф как раз запутал и ничего не показал в чём состоит баг.