Русский
Русский
English
Статистика
Реклама

Lean

Перевод Управление робототехникой в реальном времени с помощью языка Lean

09.05.2021 18:11:45 | Автор: admin

Подразделение Microsoft Research недавно опубликовало предварительный релиз Lean4. Предыдущие версии Lean были сосредоточены на том, чтобы быть помощником по доказательствам программным инструментом, который облегчает разработку строгих математических доказательств с помощью интерактивной совместной работы человека и машины. До сих пор язык Lean в основном применялся для оцифровки теоретической математики.


Главная цель Lean4 сделать Lean хорошим языком программирования, а не просто помощником по доказательствам. Синтаксис был переработан во многих отношениях, чтобы облегчить написание более широкого спектра программ. Был написан оптимизирующий компилятор, генерирующий эффективный код на языке C. Он обладает новой высокопроизводительной технологией управления памятью, помогающей избежать проблемных пауз во время работы, которые часто сопровождают такие инструменты (например сбор мусора), и при необходимости легко интегрируется с существующим кодом C/C++. В настоящее время Lean в значительной степени самодостаточный язык, который написан на самом языке Lean.

Чтобы оценить пригодность Lean как языка программирования для реальных систем, мы решили написать Lean-реализацию контроллера робототехники, работающего на одноплатном компьютере. Чтобы сделать задачу интереснее, мы выбрали контроллер для двухколёсной роботизированной платформы. Если Lean-программы не способны подавать двигателям команды в режиме реального времени в ответ на входные сигналы датчиков, система в буквальном смысле упадёт.

Наша цель состояла в том, чтобы создать работающий контроллер на языке Lean. Это отличается от того, о чем обычно думают при использовании программ для доказательства теорем. Как правило, можно указать формальную модель контроллера, которая может опустить низкоуровневые детали, определить отражающие предположения аксиомы, которые, как ожидается, будут верны для окружающей среды, а затем попытаться доказать, что контроллер стабилизировал систему в мире, удовлетворяющем аксиомам окружающей среды. Это достойная цель, и мы хотели бы в итоге её достичь. Однако, поскольку при фактической реализации контроллера для этого проекта будет использоваться язык Lean, нам необходимо было включить детали низкого уровня, которые в противном случае могут быть опущены.

Мы начали с покупки двухколёсного робота за 90 долларов и стали проводить эксперименты с языком Lean. Мы проверили сгенерированный код на языке C и библиотеку времени выполнения и обнаружили, что код вполне переносим. К сожалению, предварительный выпуск библиотеки времени выполнения Lean содержит зависимости (например от библиотеки libgmp), и она слишком велика для контроллера робота на базе Arduino. К счастью, сгенерированный код легко запускается на компьютере Rasberry Pi.

Мы приобрели 8-гигабайтную версию, чтобы скомпилировать Lean непосредственно в ней. Это добавило 80 долларов к стоимости нашего проекта, и мы вписались в наши необходимые аппаратные ограничения, а авторы Lean заинтересованы в решении проблем с размером библиотек времени выполнения.

Следующим шагом стало разделение существующего кода роботизированного контроллера для работы через последовательное соединение Bluetooth, чтобы запустить все алгоритмы управления на Rasberry Pi, сохранив при этом минимальный код для управления двигателем и считывания данных акселерометра на плате Arduino. Это было довольно просто, но потребовало использования сервиса Google Translate, чтобы понять комментарии в исходном коде. Исходный код после перевода комментариев можно посмотреть здесь, а разделённый на секции код Arduino после извлечения алгоритмов управления здесь.

fig:fig:

Затем мы транслировали код управления с языка C на язык Lean с помощью ручного, но довольно простого процесса. Версия Lean 4 в конечном счёте создаёт функциональные определения и обладает точностью, модульностью и композиционными преимуществами функционального программирования. Однако она имеет многофункциональный исходный язык, который позволяет использовать циклы for, мутабельные локальные переменные и структурированные операторы управления потоком, такие как break и continue. Внутри Lean4 использует сложный процесс анализа для автоматической и прозрачной реструктуризации кода в функциональное определение. Это снизило уровень усилий, необходимых для портирования с языка C на язык Lean.

Написанный нами код Lean доступен широкой публике на Github. Основная функция пошагового управления BalanceCar.update выполняется каждые 5мс. Для оценки ориентации робота по показаниям гироскопа и акселерометра (6 DoF IMU) используется фильтр Калмана. Контроллер PD принимает состояние ориентации в качестве входных данных и определяет скорость двигателя, таким образом замыкая контур управления.

После завершения портирования мы написали некоторый код на языке C, чтобы подключить код управления на языке Lean к последовательным API-интерфейсам Bluetooth, и опробовали его. Первоначальные результаты были занимательными, но не совсем правильными:

Это немного разочаровало, но такое случается в реальном программировании. Мы провели несколько тестов, внесли некоторые изменения, чтобы уменьшить задержку Bluetooth, и исправили в Lean-коде попутно обнаруженную ошибку. В итоге мы успешно создали работающего робота:

Как отмечалось ранее, это был всего лишь небольшой эксперимент для тестирования языка Lean в контроллере реального времени и работы, необходимой для ручного переноса кода с языка C на язык Lean. Мы ещё не проверили правильность контроллера (пока), но, когда у нас будет немного больше времени, мы планируем поработать над этим и интегрировать контроллеры на языке Lean в экосистему ROS, чтобы и другие люди могли опробовать его. У нас также есть более крупный проект, в котором языки Haskell и Lean, а также SMT-решатель используются совместно, чтобы создать проверенный декомпилятор от 64-разрядной версии с архитектурой x86 до LLVM. В будущем у нас будет больше информации об этом.

Вся работа, которую мы проделали для этого проекта, находится в открытом доступе, чтобы её могли попробовать выполнить те, кто в этом заинтересован. Мы намеренно использовали относительно недорогого робота, чтобы люди могли легко опробовать код. Так можно опробовать Lean лично или показать студентам, что вы можете писать реальные программы на этих языках. Если у вас есть какие-либо вопросы о проекте, вы можете пообщаться с нами на канале Lean Real-time Systems (Системы реального времени на языке Lean) сервиса Zulip.

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

Мы уже писали о том, как ML и компьютерное зрение используют на обогатительных фабриках, и если вы хотите научить роботов или машины видеть мир, принимать решения и действовать по ситуации, обратите внимание на наш курс "Machine Learning и Deep Learning" партнером которого является компания Nvidia.

Также можете взглянуть на профессию C++ разработчик, на котором можно прокачаться или освоить С++ с нуля. Приходите будет сложно, но интересно!

Узнайте, как прокачаться и в других специальностях или освоить их с нуля:

Другие профессии и курсы
Подробнее..

Как метрики бережливого производства можно применить в задачах технической поддержки

02.11.2020 22:09:30 | Автор: admin

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

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

Просто представьте, что у Вас сотня админов, которых Вы ежедневно обеспечиваете работой (это не выдумка, а реальность).

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

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

Можно ли с этим что-то сделать? Конечно! Работающие и очень эффективные меры давно известны это Бережливое производство (Lean Manufacturing) и Теория ограничений (Theory of Constraints, TOC).

Давайте посмотрим как методы и метрики бережливого производства могли бы послужить на благо службы технической поддержки Вашей компании.


Небольшой экскурс в Lean и TOC

Давайте начнем с краткого введения в Теорию Ограничений и Бережливое производство в том небольшом объеме, который необходим для понимания концепции этой статьи.

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

Теория ограничений это как бы надстройка над Бережливым производством, которая гласит, что в любом производстве есть всего лишь одно единственное узкое место, которое тормозит всё. И скорость всего предприятия в целом равно скорости этого узкого места (бутылочного горлышка).

Бесполезно расширять что-либо еще, кроме бутылочного горлышка это всё равно ни к чему не приведёт. Именно поэтому локальные оптимизации не работают. И именно поэтому нет смысла утилизировать мощности отделов на 100% - это только вызовет перепроизводство.

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

Это если кратко.

Единственная, но очень важная метрика теории ограничений

В Теории ограничений есть, по сути, единственная метрика, на основе которой принимаются все решения это Проход (или Проток, Throughput).

Tu=P TVC,

где Tu величина прохода на единицу продукции;
P цена единицы продукции;
TVC полностью переменные затраты

(https://tocpeople.com/2012/08/upravlenie-predpriyatiem-po-finansovym-pokazatelyam-tos/)

Если грубо, то это операционная прибыль, заложенная в конкретную единицу продукта.

Как это можно использовать?

Давайте рассмотрим известный пример с двумя продуктами. Пусть человек-бутылочное горлышко принимает участие в производстве продуктов А и Б.

Продукт А стоит 300 руб, а продукт Б 400 руб.

При этом Проход (грубо - Прибыль) продукта А = 100 руб, а у продукта Б = 200 руб

Какие продукты и в каком количестве должен производить человек-бутылочное горлышко, чтобы максимизировать прибыль предприятия (а мы знаем, что именно он определяет всю прибыль предприятия)?

NB. Вы уже провели аналогии с технической поддержкой, категориями обращений пользователей и админами, которые эти обращения выполняют?

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

Время производства продукта А 5 мин, продукта Б 30 мин.

Продукт А: 100 руб / 5 мин = 20 руб / мин

Продукт Б: 200 руб / 30 мин = 6,6 руб / мин

Получается, что при изготовлении продукта А компания получает прибыль в 20 руб/мин, а при изготовлении продукта Б всего 6,6 руб/мин.

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

Переложение метрики Прохода для технической поддержки

Самое главное сомнение, которое у Вас скорее всего возникнет в тех поддержке нет прибыли. Совершенно верно.

Дело в том, что Проход может быть не только прибылью. Он может быть чем угодно, что будет являться аналогией прибыли и что будет давать ценность компании и клиенту.

В случае с тех поддержкой несомненной ценностью является количество обращений, отработанных в установленный срок.

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

Из Jira, например, можно извлечь следующие данные:

Приоритетзадачи

Категория задачи

Общее время исполнения(от регистрации до перевода в статус Resolved) с учетом всех дней и выходных. Время исполнения с точки зрения клиента от самого начала до самого конца.

Дополнительно можно вычислить Touch time - время ручной работы админа по каждой задаче. Другими словами время, затраченное администратором на задачу за вычетом выходных, нерабочего времени и нахождения задачи в статусе Need Info (запрос доп информации от клиента).

Если на человеке висело несколько параллельных задач, то Touch time вычисляется по каждой завершенной задаче отдельно, а затем берется 85% персентиль от всего полученного множества.

Персентиль не так чувствителен к выбросам как среднее, поэтому его часто используют в качестве гарантированного значения для какого-либо параметра, в нашем случае Touch time.

В Jira значение Touch time можно вычислить как время между сменами статусов.

Время работы человека-горлышка (или время, затраченное на производства продукта) = Touch time

Проход = количество выполненных задач конкретной категории и приоритета

К прохода = Прибыль / Время работы горлышка

или

К прохода = количество выполненных горлышком задач / Touch time

Наибольшее значение коэффициента говорит о том, какой категории заявок стоит отдавать приоритет, чтобы на выходе из горлышка максимизировать общее количество выполненных заявок.

Вот реальный пример из службы тех поддержки:

Колонка template Категория задач. Строки упорядочены по убыванию коэффициента прохода.

Таблица даёт много материала для раздумий. Например, видно, что наибольшее влияние на поток оказывают задачи с низким приоритетом. Это сильно противоречит общепринятому восприятию того, что делать надо в первую очередь блокеры и высокий приоритет, и вызывает несогласие и неприятие.

Однако, если подумать нестандартно, то можно прийти к выводу, что раз задач с низким приоритетом так много, то стоит посадить выделенных людей, которые будут заниматься только ими.

Почитайте интересную статью про технологию Swarming в которой есть много подобных нестандартных выводов.

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

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

Поиск бутылочного горлышка техподдержки

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

Если просуммировать время создания ценности и соотнести его с общим временем цикла, то можно посчитать эффективность потока:

Эффективность потока = Суммарное время создания ценности / Общее время цикла * 100%

Часто эффективность потока в компаниях не превышает 5-10%.

Каким образом посчитать эффективность потока для задач тех поддержки?

Если Вы используете Jira, то можно считать время между сменой статусов и в качестве времени создания ценности брать время непосредственной работы админа, но это сложно.

Можно использовать метод проще и считать по количеству выполненных задач за период:

Эффективность потока = Кол-во выполненных задач / (Всего задач в работе) * 100%

Соответственно, такую эффективность легко посчитать по каждой категории задач, админу или команде. Т.е. Вы будете точно видеть, где именно у Вас низкая эффективность.

Вот примеры с реальными данными:

Можно отфильтровать данные по наименее эффективным группам и получить эффективность входящих в них админов.

Что обозначает эффективность потока в тех поддержке?

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

Вот пример реальной ситуации по настоящему, не выдуманному админу:

Как видите, ситуация жесткая он делает всего 4-5 задач в день, а вешают на него аж по 10 штук.

Естественно, о какой эффективности тут может идти речь.

Очень удобно анализировать подобные метрики в Qlik он позволяет последовательно сужать выборку в разных разрезах. Например, сначала выбирается категория обращений с максимальным количество незавершенного производства, затем, в её рамках, группа админов, а затем становится понятным кто из админов выбранной группы имеет наибольшую незавершенку. Таким образом можно добраться до конкретного человека и конкретной выполняемой им операции.

Как видите, метрики бережливого производства с помощью коэффициента эффективности потока, потенциально позволяют Вам обнаружить бутылочное горлышко весьма простым путем.

А если посчитать Touch time и коэффициент прохода, то можно еще и расставить приоритеты исполнения обращений, приходящих в бутылочное горлышко.

Т.е. метрики бережливого производства действительно могут помочь с налаживанием дел в технической поддержки.

Что делать со всеми этими метриками?

Улучшать, конечно. С помощью Kaizen непрерывного совершенствования. В низкой эффективность виноваты не люди виновата система. И её надо перестраивать.

Т.е. нужно находить корневую причину проблемы (истинную причину, а не лежащую на поверхности) и устранять её. И так поступать с каждой проблемой.

Вот хороший пример как в Службе Service Desk использовали Lean (бережливый подход) и что из этого получилось.

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

Зуб даю, что первое, что Вы увидите в тех поддержке - это то, что админы (/сотрудники тех поддержки) делают по десятку задач одновременно (см. график выше). Вы наверняка на себе испытали как это работает:

Клиент оставляет обращение, оно назначается на админа, а тот быстро-быстро что-то отвечает и мгновенно переводит задачу обратно с целью получения доп информации, либо переводит задачу на какого-то другого человека. И всё потому, что ему некогда ждать пока клиент ответит ему нужно сделать сегодня еще кучу задач.

Как результат, админ целый день занимается тем, что старается как можно быстрее снять с себя поступающие задачи и перевести их на клиента, а в итоге не делает ничего, либо делает чрезвычайно медленно. Типичная проблема многозадачности.

А почему у админа много задач? Корневой причиной является распространенная ложная установка. Руководство считает, что ресурсы надо утилизировать на 100%, чтобы они не простаивали. Поэтому и загружает админа задачами. Но на самом деле это заблуждение, вызывающее огромные проблемы.

При однозадачности задачи выполняются в разы быстрее, чем при многозадачности:

Решить проблему можно. Теория ограничений для этого случая говорит:

Расширьте бутылочное горлышко

Подчините ему всё производство

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

Простая перестройка процесса позволит админу выполнять только одну задачу за раз. Это может увеличить его производительность в разы:

Вариантов решений множество.

Помните, что этот админ-бутылочное горлышко, по сути, является первопричиной того, с какой скоростью и качеством Ваша служба технической поддержки обрабатывает запросы. Думайте в числах прохода. Если найм или выделение помощника этому админу увеличит проход в 5 или 10 раз, разве это не стоит того?

Возьмите одного админа-бутылочное горлышко, определите его проблему, найдите корневые причины и устраните их. Расширьте его мощность и увеличьте таким образом проход.

А на этом всё.

NB. Все выводы в этой статье сделаны на основе наблюдений за реальным отделом технической поддержки большой компании.

Автор статьи надеется, что смог показать другую точку зрения на привычные процессы и зародил в читателе зерно сомнения и инакомыслия.

Ваши комментарии он с удовольствием прочитает и ответит на них.

Подробнее..

Перевод Будущее математики?

18.07.2020 22:06:54 | Автор: admin
В этом переводе презентации британского математика Кевина Баззарда мы увидим, что следующий комикс xkcd безнадежно устарел.

image

Каково будущее математики?


  • В 1990-х компьютеры стали играть в шахматы лучше людей.
  • В 2018 компьютеры стали играть в го лучше людей.
  • В 2019 исследователь искусственного интеллекта Christian Szegedy сказал мне, что через 10 лет компьютеры будут доказывать теоремы лучше, чем люди.

Конечно, он может быть не прав. А может быть и прав.

Я верю в следующее: через десять лет компьютеры будут помогать нам доказывать муторные теоремы уровня ранних аспирантов. В каких областях математики? Зависит от того, кого получится привлечь в эту область исследования.

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

Что такое доказательство?


Если спросить студента-отличника, математика-исследователя и компьютер о том, что такое доказательство, каков будет их ответ? Ответы студента-отличника и компьютера совпадут и будут следующим:
Доказательство это логическая последовательность утверждений, состоящая из аксиом выбранной системы, правил вывода и теорем, которые были доказаны ранее, которые, в конечном итоге, приводят к доказываевому утверждению.
Конечно, ответ математика-исследователя не будет таким идеалистичным. Для математика определением доказательства будет то, что другие опытные математики считают доказательством. Или то, что принято к публикации в журналы the Annals of Mathematics или Inventiones.

Однако с этим есть небольшая проблема. Следующие скриншоты взяты с сайта журнала the Annals of Mathematics, одного из самых престижных математических журналов в мире.

image

image

Вторая статья буквально противоречит первой. Авторы открыто пишут об этом в аннотации. Насколько я знаю, the Annals of Mathematics никогда не публиковала опровержений ни одной из этих работ. Какую из работ считают правильной опытные математики? Об этом можно узнать, только если вы работаете в этой области.

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

image

Эта короткая статья 2019 года указывает на то, что другая важная статья 2015 года, опубликованная в Inventiones, в значительной степени опирается на ложную лемму. Этого никто не замечал до 2019 года несмотря на то, что в 2016 году люди устраивали семинары по изучению этой важной работы.

Владимир Воеводский, лауреат Филдсовской премии, внесший вклад в основания математики, пишет, что если автор, которому люди доверяют, пишет технически сложный аргумент, который трудно проверить, но который похож на другие, правильные, аргументы, то этот аргумент едва ли когда-нибудь будет проверен в деталях вообще.

Журнал Inventiones так и не опубликовал опровержение работы 2015 года.

Вывод: важная математика, которая была опубликована, иногда оказывается неверной. Более того, в будущем мы наверняка увидим ещё больше опровержений опубликованных доказательств.

Может быть моя работа в области p-адической программы Ленглендса опирается на неверные результаты. Или, более оптимистично, на верные результаты, но у которых нет полного доказательства.

Если наши исследования невоспроизводимы, можем ли мы это называть наукой? Я уверен на 99.9%, что p-адическая программа Ленглендса никогда не будет использована человечеством для того, чтобы сделать что-нибудь полезное. Если моя работа в математике не является полезной и не гарантирована быть верной на 100 процентов, это просто трата времени. Поэтому я решил прекратить исследования и сконцентрироваться на проверке известной математики на компьютере.

В 2019 году Balakrishnan, Dogra, Mueller, Tuitman и Vonk нашли все рациональные решения определенного уравнения четвертой степени в двух переменных. В явном виде:

$y^4 + 5x^4 - 6x^2y^2 + 6x^3 + 26x^2y + 10xy^2 10y^3 32x^2 2 -40xy + 24y^2 + 32x 16y = 0.$


Это вычисление имеет важное приложение в арифметике. Доказательство существенным образом опирается на вычисление в magma (система с закрытым исходным кодом), использующая быстрые нереферируемые алгоритмы. С большим трудом можно было бы перенести все вычисления на систему с открытым исходным кодом, например, sage. Однако никто не планирует этого делать.

Таким образом, часть доказательства остаётся скрытой. И возможно навсегда останется скрытой. Является ли этой наукой?

Пробелы в математике


  • В 1993 году Эндрю Уайлс объявил о доказательстве Великой теоремы Ферма. В доказательстве был пробел.
  • В 1994 году Уайлс и Ричард Тейлор устранили пробел, работа была опубликована и принята в математическом сообществе.
  • В 1995 году я указал Тейлору, что их доказательство использует работу Гросса, которая была не завершена. В работе Гросса было предположение, что линейные операторы Гекке, определенные на канонически изоморфных группах когомологий, коммутируют с каноническим изоморфизмом. Тейлор ответил мне, что с этим нет проблем, потому что он знает другой аргумент, который не опирается на работу Гросса.

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

А что если методы сильны, а авторы нет? Так возникают ситуации, когда наши доказательства не полны. Так возникают споры о том, доказаны ли наши теоремы на самом деле. Это совсем не то, как мы рассказываем о математике нашим студентам.

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

Большие пробелы в математики


Экспонат A


Классификация простых конечных групп. Эксперты утверждают, что у нас есть законченная классификация простых конечных групп. Я верю экспертам.

  • В 1983 году было объявлено о доказательстве классификации экспертами.
  • В 1994 году эксперты нашли ошибку (но давайте не будем раздувать из мухи слона?)
  • В 2004 году была опубликована 1000+ страничная работа. Эксперт в области Aschbacher утверждает, что ошибка была исправлена и объявляет план о публикации 12 томов полного доказательства.
  • В 2005 году только 6 из 12 томов было опубликовано
  • В 2010 году только 6 из 12 томов было опубликовано
  • В 2017 году только 6 из 12 томов было опубликовано
  • В 2018 году были опубликованы 7-й и 8-й тома и заметка о том, что публикация будет доделана к 2023 году.

Из трёх людей, руководящих проектом, один умер. Двум другим уже за семьдесят.

Экспонат B


Потенциальная модулярность абелевых поверхностей. Год назад мой выдающийся аспирант Toby Gee с тремя соавторами опубликовали 285-страничный препринт с результатом о том, что абелевы поверхности над тотально действительными полями являются потенциально модулярными.

Их доказательство цитирует три неопубликованных препринта (один 2018 года, один 2015 года, один 1990-х годов), записки 2007 года из интернета, неопубликованную диссертацию на немецком и работу, чьё главное утверждение было позднее опровергнуто. Более того, на 13 странице мы видим следующий текст:
Мы хотим обратить внимание на то, что мы используем Arthurs multiplicity formula для дискретного спектра GSp4, которая была объявлена в [Art04]. Доказательство, опирающееся на другие работы автора о симплектической и ортогональной группах, было дано в [GT18], но их доказательство имеет те же предположения, что и результаты в работе [Art13] и [MW16a, MW16b]. В частности, оно зависит от случаев twisted weighted fundamental lemma, которая была объявлена в [CL10], но доказательство которых ещё не было найдено. Более того, мы опираемся на ссылки [A24], [A25], [A26] и [A27] из работы [Art13], который на момент написания статьи ещё не опубликованы.
Может ли мы честно утверждать, что это наука?

Ссылка [CL10] выглядит следующим образом:
image
Работа, которая нужна моему аспиранту и соавторам так и не опубликована. Скорее всего, утверждение верно. Возможно даже доказуемо.

А это упомянутые ссылки из работы [Art13]:
image

В прошлом году я спросил Arthur про эти ссылки, и он ответил мне, что ни одна из работ еще не готова. Конечно, Jim Arthur гений. Он выиграл множество престижных наград. Но ему также 75 лет.

Экспонат C


GaitsgoryRozenblyum. В последнее время бесконечные категории обрели популярность. Со временем они станут ещё более важными. Работа Филдсовского лауреата Петера Шольце опирается на бесконечные категории.

Джейкоб Лурье написал 1000+ страничную работу об $(\infty, 1)$-категориях и включил много деталей в свою работу. GaitsgoryRozenblyum хотели получить аналогичных результаты про $(\infty, 2)$-категории, но в целях экономии времени опустили многие аргументы. Опущенные доказательства появятся где-нибудь ещё.

Я спросил Gaitsgory, как много было пропущено. Он ответил, что около 100 страниц. Я спросил Лурье, что он думает на этот счёт. Он ответил, что математи сильно различаются по тому, насколько комфортно для них опускать детали.

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

На конференции в университете Карнеги-Меллона, где я был на прошлой неделе, Markus Rabe рассказал мне, что Google работает над программой, которая будет переводить математические препринты с arxiv.org на язык, возможный для компьютерной проверки. А ещё я недавно видел работу, которая опирается на статью моего ученика, но ничего не упоминает про опущенные 100 страниц в [Art13].

Ошибка напоследок


image
Это очень интересный пример. Оригинальная работа была опубликована в журнале J. Funct. Anal. в 2013 году. В работе присутствует большая ошибка (неравенство в другую сторону). Ошибка была обнаружена S. Gouezel в 2017 году, когда Gouezel формализовал аргумент, используя компьютерную программу для проверки доказательств (Isabelle).

Новый аргумент представлен Gouezel и автором оригинальной работы. Новая работа не нуждается в рецензировании. Компьютер проверил 100 процентов нового аргумента. Методы оказались достаточно сильными, чтобы доказать теорему. И под доказательством я имею в виду классическое, чистое, определение доказательства то, которому мы учим наших студентов. Каждая деталь доказательства доступна читателю. Наука воспроизводима. Это математика, которую мы преподаем нашим студентам. Это и есть математика.

Вот другие примеры того, что, по-моему, является математикой:
  • Типичное доказательство уровня студента или магистра
  • Типичное доказательство столетней давности важного результата, который был хорошо задокументирован и исследован десятками тысяч математиков
  • Формальные доказательства авторства следующих математиков: Gonthier, Asperti, Avigad, Bertot, Cohen, Garillot, Le Roux, Mahboubi, OConnor, Ould Biha, Pasca, Rideau, Solovyev, Tassi и доказательство Thry теоремы FeitThompson
  • Формальное доказательство авторства следующих математиков: Hales, Adams, Bauer, Dat Tat Dang, Harrison, Truong Le Hoang, Kaliszyk, Magron, McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Nipkow, Obua, Pleso, Rute, Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Urban, Ky Khac Vu и доказательство Zumkeller гипотезы Кеплера.



На этом текст презентации заканчивается, потому что Кевин переходит к своей главной части: формальная верификация математических доказательств в системе Lean, разработанной Leo de Moura в Microsoft Research. К сожалению, примеры не вошли в слайды.

image

Автор огромный энтузиаст формальной верификации математических доказательств и ведёт очень интересный блог Xena на эту тему, который я очень рекомендую.
Подробнее..

Компьютерное доказательство теории конденсированной математики первый шаг к великому объединению

20.06.2021 16:11:04 | Автор: admin

Пример расчётного доказательства в Lean

Математики давно используют компьютеры в своей работе как инструменты для сложных вычислений и выполнения рутинных операций перебора. Например, в 1976 году методом компьютерного перебора была доказана теорема о четырёх красках. Это была первая крупная теорема, доказанная с помощью компьютера.

Теперь вспомогательный софт для доказательства теорем (proof assistant software) не просто для проверяет доказательства, но помогает выйти на принципиально новый уровень великого объединения разных математических разделов. Концепция конденсированной математики обещает принести новые идеи и связи между областями, начиная от геометрии и заканчивая теорией чисел. Это в своём роде великое объединение математики

Впрочем, обо всём по порядку.

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

Петер Шольце хочет ни больше ни меньше перестроить большую часть современной математики, начиная с одного из её краеугольных камней топологии. И теперь благодаря компьютерной инструменту автоматического доказательства теорем под названием Lean он получил подтверждение, лежащее в основе его поисков, пишет Nature.

Конденсированная математика


Амбициозный план Петер Шольце разработал совместно с коллегой Дастином Клаузеном из Копенгагенского университета и изложил в серии лекций по аналитической геометрии (pdf) в в 2019 году в Боннском университете (Германия), где они работают.

По мнению коллег, если замысел Шольце будет реализован, то через 50 лет преподавание математики аспирантам может сильно отличаться от сегодняшнего. Мне кажется, есть много областей математики, на которые повлияют его идеи, говорит Эмили Риль, математик из Университета Джона Хопкинса в Балтиморе.

До сих пор большая часть аналитической геометрии Шольце опиралась на техническое доказательство, настолько сложное, что даже сами авторы не были уверены в его корректности. Но 5 июня 2021 года Шольце объявил в блоге о завершении работы по компьютерному доказательству!

Великое объединение


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

Топология играет важную роль не только в геометрии, но и в функциональном анализе, изучении функций. Функции обычно живут в пространствах с бесконечным числом измерений (например, волновые функции, которые являются основой квантовой механики). Это также важно для систем чисел, называемых p-адическими числами, которые имеют экзотическую, фрактальную топологию.

Примерно в 2018 году Шольце и Клаузен начали понимать, что традиционный подход к понятию топологии приводит к несовместимости этих трёх математических вселенных геометрии, функционального анализа и p-адических чисел, но можно попробовать устранить эти пробелы.

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


Но если определить топологию правильным образом, то аналогии между теориями окажутся примерами одной и той же конденсированной математики, пишет Nature. Это своего рода великое объединение трёх областей.

Шольце и Клаузен уже нашли конденсированные доказательства ряда глубоких геометрических фактов и теперь могут доказать теоремы, которые ранее были неизвестны. Правда, они ещё не обнародовали эти данные.

Теорема


Суть поставленной задачи Шольце подробно изложил в декабре 2020 года. Он поставил задачу доказать очень теорему о множестве вещественных чисел, которое имеет топологию прямой линии. Это как бы основополагающая теорема, которая позволяет вещественным числам войти в эту новую структуру, объясняет Коммелин.



Работа по доказательству получила название Liquid Tensor Experiment, по имени любимой рок-группы математиков.

Вспомогательный софт для доказательства теорем


Вспомогательный софт для доказательства теорем (proof assistant software) используется уже десятилетиями. Если вкратце, то пользователь вводит в систему утверждения, которые дают машине определения математических понятий объектов на основе более простых объектов, о которых машина уже знает. Это утверждение может просто ссылаться на известные объекты. Затем программа ответит, является ли данный факт очевидно истинным или ложным, основываясь на своих текущих знаниях.

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

Из самых известных систем такого типа Isabelle, Lean, Mizar и Coq, см. более полный список.

В данном случае математики решили использовать программу Lean и кодирование всех необходимых понятий и объектов заняло полгода. Естественно, Шольце работал не в одиночку. Ему помогала группа добровольцев под руководством Йохана Коммелина, математика из Фрайбургского университета в Германии.


Числовая прямая, показано положение на ней чисел $2$, $e$ и $\pi$

По словам одного из помощников Йохана Коммелина, Lean-версия доказательства Шольце включат десятки тысяч строк кода она примерно в 100 раз больше, чем оригинальная версия: Если вы просто посмотрите на код Lean, вам будет очень трудно понять доказательство, особенно в его нынешнем виде. Но исследователи говорят, что потраченные усилия, заставить доказательство сработало в программе, помогли им лучше понять саму теорему и доказательство.

Вообще, кодирование теоремы в программе для автоматического доказательства помогает понять, что построение теоремы и её доказательство по сути одно и то же.

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

Так или иначе, но данный случай доказывает, что программы для доказательства теорем действительно способны помочь в особо тяжёлых случаях. Похоже, компьютер способен одновременно оперировать с большим количеством объектов, чем оперативная память человека. После того, как в течение полугода, в программу вводили объекты, она всё-таки смогла выстроить логическую цепь и подтвердить доказательство.


Выдача Lean по доказательству теоремы Шольце и Клаузена

У таких программ есть свои поклонники, но это первый случай, когда они сыграли важную роль во фронтире математической науки, говорит Кевин Баззард, математик из Имперского колледжа Лондона, который участвовал в совместном проекте по проверке результатов Шольце и Клаузена. До сих пор в воздухе висел главный вопрос: справятся ли они со сложной математикой? Мы показали, что справятся.

Специалисты говорят, что полгода кодирования в Lean даже небольшой срок для такой монументальной задачи. Софт для доказательства теорем доказал, что за разумный промежуток времени может формально проверить сложнейшее оригинальное исследование.



VPS серверы от Маклауд быстрые и безопасные.

Зарегистрируйтесь по ссылке выше или кликнув на баннер и получите 10% скидку на первый месяц аренды сервера любой конфигурации!

Подробнее..

Как скрам помогает стать более сильным разработчиком?

28.11.2020 00:23:46 | Автор: admin

Тема методологий и процессов разработки, как правило, не особо интересна разработчикам. Абсолютно нормально услышать: Должен быть менеджер, который этим занимается. Как мне кажется, большинство разработчиков попросту не видят достаточно ценности в том, чтобы понимать процессы компании. Однако, по моему опыту, это крайне важный компонент, который позволяет программистам становиться сильнее именно с технической точки зрения, а также двигаться по карьерной лестнице вверх. Эту связь я и попытаюсь показать.

 Copyright Max Degtyarev (http://personeltest.ru/aways/www.behance.net/maxdwork) Copyright Max Degtyarev (http://personeltest.ru/aways/www.behance.net/maxdwork)

Если спросить программиста, то как правило, его будут заботить в основном знание какого-либо языка программирования, платформы, фреймворка, алгоритмов и структур данных, паттернов и принципов проектирования. В мире это принято называть Hard Skills.

Что до Soft skills, то, к сожалению, это считается чуть ли не лишним ингредиентом, пустой тратой времени, или же несущественным элементом. Ценность Hard Skills сильно выше, чтобы переставать работать с человеком из-за проблем с Soft Skills.

И об этом можно легко сделать вывод, пройдя несколько собеседований в компаниях, где часто можно встретить человека, активно пытающегося "завалить" интервьюируемого техническими вопросами, дабы показать его слабости. В некоторых компаниях под конец беседы могут спросить о хобби. Ну и упомянуть что используют Agile. Однако по факту, большинство разработчиков участвуют в необходимых церемониях постольку поскольку, лишь бы к ним не приставали надоедливые менеджеры или скрам мастера.

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

Однако, разработчики, которые пытались хотя бы раз создать продукт для конечного потребителя, должны знать о том, как много вещей необходимо сделать и учесть: продуманный UX, дружественный UI, хорошая производительность и стабильность, безопасность, доступность, и так до бесконечности.

Как правило, это нужно умножить на количество платформ, на которых вы строите продукт. А ещё, добавить лицензирование, маркетинг, поддержку, обработку баг репортов и запросов на новую функциональность. Ну и конечно, в некоторых область, нужно добавить прессинг со стороны конкурентов.

Итого: строить продукт сложно и дорого. Крайне сложно удержать в одной голове все эти моменты, а потому продукты строят, как правило, команды, а не личности.

Цель

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

Однако, здесь не достаёт чуточку цели.

Одна из очевидных целей любой коммерческой организации - заработок денег в обмен на продукты или экспертизу, которую они поставляют на рынок. Работники компаний формируют команды, а они, подобно оркестру, исполняют свои обязанности в нужном количестве и качестве, а главноев срок.

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

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

Итерации

Люди не любят покупать некачественные продукты. Ещё меньше людей любят покупать товары, которые не выполняют того, для чего они предназначены. Однако, создать с ноля крутой, качественный и тем более идеальный продукт невозможно, без достаточных инвестиций денег, времени и умений.

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

Иногда компании решают полностью развернуть продукт на 180 градусов, или остановить производство, поняв, что идут совершенно не туда. Это происходит в основном потому, что менеджмент компании пытается соблюсти баланс между инвестициями на производство и доходом, который в итоге получится.

Очень важно сделать поворот в правильный момент времени, пока ещё не поздно или не слишком рано. Хорошо угаданный момент позволяет организации усилить более перспективные направления.

Если что-то из вышесказанного кажется недостаточно аргументированным, то я хочу порекомендовать вам набор статей по Theory of constraints, который содержит выборку необходимой и достаточной информации по выше изложенным фактам.

Для разработчиков из всего вышеизложенного важно одно: направление развития продукта (и компании) будет меняться, точно!

Работая в стартапах сложно сказать какую проблему придётся решать через 6 месяцев. Никто не знал, что видео-сервис для свиданий станет самым популярным в мире видео-стриминговым сервисом YouTube. Так же, как никто не предполагал, что игра для социализации может превратиться в чат для коллег, как в случае Slack. Бизнесы, которые не смогли повернуть свои продукты в правильном направлении, либо уже исчезли, либо близки к провалу.

Пример плохого развития событий в фазовом подходе Waterfall.Пример плохого развития событий в фазовом подходе Waterfall.

Гибкие методология стали появляться как раз-таки на волне понимания, как важно сохранить возможность гибкости стратегии, возможность в нужный момент резко повернуть в сторону, а не продолжать двигаться по длинным фазам, делая проект, в целях которого уже не уверен. Одним из важнейших отличий гибких методологий от фазовых подходов, вроде Waterfall, являются короткие итерации. Укажу лишь несколько причин по которым организация может видеть итерации полезными:

  • Возможность скорректировать путь развития продукта, определив новое направление или возможности заработка.

  • Снизить потери в случае неправильных решений или не оправдавших себя ожиданий.

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

Конечно, когда продукт развивается короткими итерациями, то очень часто нельзя сделать полное решение задачи в одну итерацию. Работа делится на части и само собой появляется требование доставлять продукт инкрементально: всё больше и больше функций с каждой итерацией.

 Пример инкрементальной доставки изменений в продукте. Пример инкрементальной доставки изменений в продукте.

Как неудивительно, это требование должны удовлетворить разработчики, создав соответствующую архитектуру продукта.

Гибкая архитектура

Есть одна фундаментальная вещь, которую нужно понять с точки зрения разработки: преждевременное принятие решений (up-front design)это не всегда хорошо, а чаще плохо.

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

Итеративный подход Scrum ставится в противовес фазовому Waterfall, но так как это не является темой моих рассуждений, я приведу отличную статью на этот счёт.

Самое важное, что нужно понять программисту, это то, что решения бывают 2х видов:
1. Решения, которые можно легко откатить назад
2. Решения, которые нельзя просто откатить назад

Последние как раз и являются самыми проблематичными. И когда я говорю про Up-Front design, подразумевается именно ряд решений, которые невозможно или слишком долго повернуть вспять.

В архитектуре программного обеспечения нужно оставлять возможность принять критическое решение как можно позже в цикле жизни продукта. Чем позже это решение будет сделано, тем у вас будет больше данных, подтверждающих его правоту. Приведу несколько примеров:

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

  2. Выбрав фреймворк для написания программы, подумали ли вы насколько легко будет переключиться на другой фреймворк в случае необходимости?

  3. Если вы выбрали для разработки новый язык программирования, вы точно сможете найти себе знающих коллег, которые смогут вместе с вами поддерживать и развивать продукт?

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

Если вы или ваши коллеги уже применяете такого рода анализ, тогда возможно вы уже в безопасности.

Ещё один сложный вопрос: как вести разработку в условиях изменяющихся требований? Изменяющиеся требования среди разработчиков принято считать чем то очень плохим.
Это происходит из-за того, что необходимость менять требования заложена в понятие программного (Softгибкий) обеспечения, но не указана явно.

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

Каждый уважающий себя разработчик должен прочитать книгу Чистая Архитектура Роберта Мартина, в которой эта тема раскрыта очень широко и приведены примеры решений:

When requirements change, the difficulty in making such a change should be proportional to the scope of the change, not to the shape of the change. The difference between scope and shape often drives the growth in software development costs. It is the reason that the first year of development is much cheaper than the second, and the second year is much less expensive than the third.

The goal of software architecture is to minimize the human resources required to build and maintain the required system.

Robert C. Martin, Clean Architecture: A Craftsmans Guide to Software Structure andDesignRobert C. Martin, Clean Architecture: A Craftsmans Guide to Software Structure andDesign Роберт Мартин, Чистая Архитектура: искусство разработки программного обеспечения. Роберт Мартин, Чистая Архитектура: искусство разработки программного обеспечения.

Позвольте добавить один совет, которого в книге нет: разработчики должны создавать настолько мало кода, насколько это вообще возможно, а в идеале вообще обойтись без кода. При этом нужно всё также добавлять функционал. Феноменально, не правда ли?

Нет, я не говорю перестать писать код вообще и перейти на готовые конструкторы. И нет, я не говорю перестать создавать ПО. Я говорю о том, чтобы начать делать ровно то, что приносит ценность, и перестать делать то, что только отнимает усилия. Вот некоторые факты:

  • Меньше нового кода, означает меньше поддержки.

  • Меньше нового кода также означает меньше всего что может сломаться (работает, не трогай! помните?).

  • Меньше нового кодаменьше когнитивной нагрузки.

  • Меньше нового кодабольше уверенности в результате работы.

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

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

  2. Ровно так же, не стоит писать свой код реализации шифрования. Не стоит писать код там, где вы не являетесь специалистом. Ваши пользователи, как и бизнес, этого не оценят.

Может быть этот совет и покажется кому-то теоретическим. Однако, с практикой и опытом, всё больше начинаешь замечать моменты, в которых лучшее решение лежит совсем не в коде. Как инженеры с развитым системным мышлением, вы можете помочь команде и указать на подобные решения.


Если говорить о коде, то программисты нанимаются для того, чтобы вносить изменения в поведение программного обеспечения так быстро, насколько это возможно. Разработчики могут поддерживать скорость изменений на достаточном уровне только создавая достаточно гибкую архитектуру. Для этого требуется своевременная коммуникация с бизнесом для выяснения что на самом деле ему надо. Также, требуется тщательно продумывать каждое изменение, контролируя архитектуру и технический долг, и постоянно уточняя требования. Если не обратить внимание хотя бы на одну из этих составляющих (перестать коммуницировать с бизнесом или же не обращать внимание на архитектуру), то так или иначе, но скорость внесения изменений очень быстро упадёт, и к вам возникнут вопросы. В последнее время всё чаще встречаются термины Agile Architecture и Lean Architecture. Я предпочитаю объединить эти понятия в одном термине: Гибкая архитектура.

Понятия Гибкой архитектуры и Чистой архитектуры на самом деле идут рука об руку. С одной стороны, важно понимать проблемы бизнеса и закладывать возможности расширения исходя из непредсказуемости некоторых областей в бизнесе. С другой стороны, нужно использовать наработанные известные практики при проектировании. А чтобы их использовать, программист должен учиться, расти и становиться сильнее.

Сильный разработчик

Понятие очень размытое и меняет своё значение от компании к компании, от бизнеса к бизнесу, и от команды к команде. Оно часто зависит от мнения начальства, менеджеров, и вообще коллег. Soft skills как раз нужны для того, чтобы это мнение было положительным. Но многим разработчикам эти навыки даются нелегко. Зато, одно остаётся верным всегда: сильный разработчик тот, кто умеет проектировать программное обеспечение, которое соответствует нуждам бизнеса.

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

Это сложная задача. Придётся очень многое учить, узнавать принципы проектирования, постоянно практиковаться и использовать выученные навыки. В критические моменты придётся аргументированно говорить бизнесу о необходимости работы над архитектурой и уменьшением технического долга. И уж точно будет не мало трудных моментов в решении конкретных задач по проектированию.

Представьте, насколько сильно изменилась архитектура Android, который изначально был задуман как операционная система для камер, и только. А теперь это одна из двух самых популярных мобильных платформ. Другой пример, PayPal, который создавался как сервис перевода денег между телефонов с операционной системой Palm OS. А теперь сервис обрабатывает миллионы платежей по всему миру.
Врядли, развитие кодовой базы этих проектов было монотонным ростом функционала из года в год. Уверен, что такие изменения, словно большой взрыв, порождают массу работ по адаптации, рефакторингу и переписыванию с ноля. Это конечно одни из самых сложных случаев. Но кто может заранее предположить путь вашего проекта?

А где жескрам?

После того как я провёл параллели между необходимостью бизнеса и техническими навыками разработчиков, а также поверхностно описал трудоёмкость стоящих перед разработчиком задач, думаю настало время суммировать, чем же именно правильно интегрированный скрам поддерживает технический навыки разработчиков. Да, я не оговорился, именно правильно интегрированный скрам. Я видел примеры плохой интеграции методологий, но видел и успешные случаи. С полной ответственностью могу сказать, что одно без другого не получится. Итак:

  • Скрам позволяет командам понимать цели бизнеса. Команды, как правило, знают ответы на вопросы Зачем мы делаем это?, Как именно мы должны это сделать?, Что будет показателем успеха нашей работы? и т.д.
    Эти вопросы могут задаваться не сразу, не с первого дня, но так или иначе, команды приходят к ним. И получают ответы.


    Имея эти ответы, разработчики могут проектировать системы с большей уверенностью в правильности действий, верно определять интерфейсы взаимодействия компонент, создавать слабосвязанные и мало-зависимые друг от друга компоненты. Такое проектирование повышает качество и стабильность конечного продукта.

  • Скрам позволяет командам действовать независимо, самостоятельно принимать решения и не бояться пробовать новые идеи. Представьте, что вы приняли неверное решение в одной из 2-недельных итераций, внесли изменения, а во время презентации работы выяснились неожиданные подробности.


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

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


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

Вывод

Некоторые путают понятия Спецификация и Требования. На самом деле, Спецификация может лишь формально описать пожелания заказчика. Но Требования - понятие более широкое. Оно включает и сам процесс разработки, и процесс доставки, и то, как часто и где будет необходимо менять поведение системы. И даже тот факт, кто запрашивает эти изменения. Поначалу, какие-то из этих деталей могут казаться не относящимися к архитектуре совсем, но через некоторое время стать важнейшими и критическими требованиями к системе. Всё должно быть отражено в программной архитектуре.

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

Подробнее..

Категории

Последние комментарии

  • Имя: Макс
    24.08.2022 | 11:28
    Я разраб в IT компании, работаю на арбитражную команду. Мы работаем с приламы и сайтами, при работе замечаются постоянные баны и лаги. Пацаны посоветовали сервис по анализу исходного кода,https://app Подробнее..
  • Имя: 9055410337
    20.08.2022 | 17:41
    поможем пишите в телеграм Подробнее..
  • Имя: sabbat
    17.08.2022 | 20:42
    Охренеть.. это просто шикарная статья, феноменально круто. Большое спасибо за разбор! Надеюсь как-нибудь с тобой связаться для обсуждений чего-либо) Подробнее..
  • Имя: Мария
    09.08.2022 | 14:44
    Добрый день. Если обладаете такой информацией, то подскажите, пожалуйста, где можно найти много-много материала по Yggdrasil и его уязвимостях для написания диплома? Благодарю. Подробнее..
© 2006-2024, personeltest.ru