Forwarded from Команда T1
Митапы для разработчиков или для аналитиков? А что, если сделать два в одном флаконе 🧪
Объединяемся большим сообществом коллег на самом ламповом митапе Т1 Лампа: Анализ + разработка = 🤝 уже 27 февраля в Рязани!
Обсудим, как оптимально выстроить взаимодействие между аналитиками и разработчиками, как оптимизировать ресурсы в IT-инфраструктурах и разграничивать задачи между разными командами. Участие бесплатное и офлайн — регистрируйтесь по ссылке, но выбирайте кнопку «Очное+Онлайн».
⌛ 27 февраля, 19:00
📍 Рязань, ул. Соборная, 15А, пространство «Панорама»
Уже готовы встречать гостей из всех городов 💙
#апдейтТ1@t1career
Объединяемся большим сообществом коллег на самом ламповом митапе Т1 Лампа: Анализ + разработка = 🤝 уже 27 февраля в Рязани!
Обсудим, как оптимально выстроить взаимодействие между аналитиками и разработчиками, как оптимизировать ресурсы в IT-инфраструктурах и разграничивать задачи между разными командами. Участие бесплатное и офлайн — регистрируйтесь по ссылке, но выбирайте кнопку «Очное+Онлайн».
Уже готовы встречать гостей из всех городов 💙
#апдейтТ1@t1career
Please open Telegram to view this post
VIEW IN TELEGRAM
Please open Telegram to view this post
VIEW IN TELEGRAM
C++ и неопределённое поведение
27 февраля 14:00
Мы пригласили в гости Дмитрия Свиридкина — автора книги "Путеводитель C++ программиста по неопределённому поведению". Обсудим грани, отделяющие корректный C++ код от некорректного, попросим рассказать историю написания книги, поговорим о развитии языка и его будущем.
27 февраля 14:00
Мы пригласили в гости Дмитрия Свиридкина — автора книги "Путеводитель C++ программиста по неопределённому поведению". Обсудим грани, отделяющие корректный C++ код от некорректного, попросим рассказать историю написания книги, поговорим о развитии языка и его будущем.
Forwarded from Антиконференция Summer Merge
Предложение для всех, кто влюблен в IT и загородный отдых
14 февраля при покупке одного билета на самую летнюю IT-тусовку Summer Merge вы получаете от нас второй билет в подарок 🎁
Предложение ограничено и действует только 1 день.
📍Важно: обязательно укажите корректную почту, и мы вышлем на неё второй билет в течение недели.
Только вам решать, с кем провести незабываемый летний уикенд!
Антиконференция Summer Merge — это три дня продуктивного нетворкинга в окружении красивейших видов волжского залива.
Встречаемся 20-22 июня в эко-парке Русский Берег ❤️🔥
👉 Купить билет и узнать подробности
14 февраля при покупке одного билета на самую летнюю IT-тусовку Summer Merge вы получаете от нас второй билет в подарок 🎁
Предложение ограничено и действует только 1 день.
📍Важно: обязательно укажите корректную почту, и мы вышлем на неё второй билет в течение недели.
Только вам решать, с кем провести незабываемый летний уикенд!
Антиконференция Summer Merge — это три дня продуктивного нетворкинга в окружении красивейших видов волжского залива.
Встречаемся 20-22 июня в эко-парке Русский Берег ❤️🔥
👉 Купить билет и узнать подробности
Поддержка команды, стресс-менеджмент, эффективность в кризис — ключевые задачи тимлида в эпоху турбулентности.
Как с этим справляться? Разбираемся на онлайн-конференции Podlodka Teamlead Crew (10-14 марта)🔥
Что ждать в программе:
📢 Как повысить эффективность команды, когда её требуют повысить - Астислав Божевольнов (Cardooworld) на примере реального кейса расскажет, как можно принять сложное решение, не сломаться под давлением и найти точки роста.
⚖ Как найти опору для себя, когда ты опора для команды - Дарья Шалагина (Точка) поделится проверенным методом самоподдержки для тимлидов в условиях высоких требований и перегрузок.
🚀Как поддерживать команду в тяжёлый момент - эксперты из Точки, Selectel, Туту и Инфосистемы Джет на примерах разберут, как помочь команде справляться с кризисами.
🎰 Рулетка кейсов: Когда тимлиду пора сваливать - Евгений Кот и Артём Малышев помогут разобраться в кризисных ситуациях. Анонимно делимся ситуацией, получаем честный разбор и совет — бежать или оставаться.
И многое другое! Билеты уже в продаже: https://podlodka.io/tlcrew
Как с этим справляться? Разбираемся на онлайн-конференции Podlodka Teamlead Crew (10-14 марта)🔥
Что ждать в программе:
📢 Как повысить эффективность команды, когда её требуют повысить - Астислав Божевольнов (Cardooworld) на примере реального кейса расскажет, как можно принять сложное решение, не сломаться под давлением и найти точки роста.
⚖ Как найти опору для себя, когда ты опора для команды - Дарья Шалагина (Точка) поделится проверенным методом самоподдержки для тимлидов в условиях высоких требований и перегрузок.
🚀Как поддерживать команду в тяжёлый момент - эксперты из Точки, Selectel, Туту и Инфосистемы Джет на примерах разберут, как помочь команде справляться с кризисами.
🎰 Рулетка кейсов: Когда тимлиду пора сваливать - Евгений Кот и Артём Малышев помогут разобраться в кризисных ситуациях. Анонимно делимся ситуацией, получаем честный разбор и совет — бежать или оставаться.
И многое другое! Билеты уже в продаже: https://podlodka.io/tlcrew
Регистрация
Узнаем об опасных местах и областях применения пакета unsafe. Обеспечим высокопроизводительную конкурентность в Go. А в рамках дискуссии узнаем, что нового появилось в Go 1.24 и как это повлияет разработку.
Офлайн-участников будет ждать демозона с «железом» для ЦОД и телеком-операторов, которое создают инженеры YADRO, технические интерактивы и подарки от компании.
● От мьютексов к lock-free: как обеспечить высокопроизводительную конкурентность в Go
На первый взгляд мьютексы кажутся простыми, но это не так. В своем докладе я предлагаю заглянуть «под капот» и разобраться, как они работают, почему не так легковесны, как кажется, и в каких случаях могут стать узким местом. Также рассмотрим альтернативу мьютексам — lock-free структуры — и обсудим, когда их использование может повысить производительность вашего приложения.
Доклад будет полезен тем, кто хочет глубже погрузиться в конкурентность в Go, разобраться в работе мьютексов и изучить доступные альтернативы.
Илья Уваркин, инженер-программист в департаменте разработки унифицированной системы хранения данных, YADRO
● Погружение в мир без правил с пакетом unsafe
Многие считают, что unsafe-код — это сложно или что он ведет к ошибкам. Так ли это?
Я расскажу о пакете unsafe, опасных местах и областях применения. На конкретных примерах мы увидим, как оптимизировать структуры, получать доступ к скрытым полям и преобразовывать данные для работы с промышленными протоколами. Рассмотрим основные компоненты пакета unsafe, затронем вопросы адресной арифметики и преобразования типов.
Нина Пакшина, Go-разработчик
● Go 1.24: Куда движется язык?
Что нового появилось в стандарте языка и как это повлияет разработку? Мы обсудим важнейшие изменения: от механизма отслеживания зависимостей до слабых указателей (weak pointers) в стандартной библиотеке. Разберемся, как новые возможности, такие как флаг -json, улучшенные финализаторы, пакет crypto/mlkem и многое другое могут изменить подход к разработке.
Даниил Подольский, эксперт по разработке ПО и один из лидеров внутреннего Go-сообщества, YADRO
Александр Иванов, старший инженер-программист, YADRO
Павел Агалецкий, ведущий инженер в платформе, AvitoTech
Игорь Панасюк, Go-разработчик, Yandex. Преподаватель, ИТМО
Узнаем об опасных местах и областях применения пакета unsafe. Обеспечим высокопроизводительную конкурентность в Go. А в рамках дискуссии узнаем, что нового появилось в Go 1.24 и как это повлияет разработку.
Офлайн-участников будет ждать демозона с «железом» для ЦОД и телеком-операторов, которое создают инженеры YADRO, технические интерактивы и подарки от компании.
● От мьютексов к lock-free: как обеспечить высокопроизводительную конкурентность в Go
На первый взгляд мьютексы кажутся простыми, но это не так. В своем докладе я предлагаю заглянуть «под капот» и разобраться, как они работают, почему не так легковесны, как кажется, и в каких случаях могут стать узким местом. Также рассмотрим альтернативу мьютексам — lock-free структуры — и обсудим, когда их использование может повысить производительность вашего приложения.
Доклад будет полезен тем, кто хочет глубже погрузиться в конкурентность в Go, разобраться в работе мьютексов и изучить доступные альтернативы.
Илья Уваркин, инженер-программист в департаменте разработки унифицированной системы хранения данных, YADRO
● Погружение в мир без правил с пакетом unsafe
Многие считают, что unsafe-код — это сложно или что он ведет к ошибкам. Так ли это?
Я расскажу о пакете unsafe, опасных местах и областях применения. На конкретных примерах мы увидим, как оптимизировать структуры, получать доступ к скрытым полям и преобразовывать данные для работы с промышленными протоколами. Рассмотрим основные компоненты пакета unsafe, затронем вопросы адресной арифметики и преобразования типов.
Нина Пакшина, Go-разработчик
● Go 1.24: Куда движется язык?
Что нового появилось в стандарте языка и как это повлияет разработку? Мы обсудим важнейшие изменения: от механизма отслеживания зависимостей до слабых указателей (weak pointers) в стандартной библиотеке. Разберемся, как новые возможности, такие как флаг -json, улучшенные финализаторы, пакет crypto/mlkem и многое другое могут изменить подход к разработке.
Даниил Подольский, эксперт по разработке ПО и один из лидеров внутреннего Go-сообщества, YADRO
Александр Иванов, старший инженер-программист, YADRO
Павел Агалецкий, ведущий инженер в платформе, AvitoTech
Игорь Панасюк, Go-разработчик, Yandex. Преподаватель, ИТМО
SAST как Quality Gate
13 марта 14:00
Использование SAST в качестве Quality Gate — это не просто тренд, а необходимость для современных разработчиков, стремящихся создавать надежные и безопасные приложения. Узнайте, как внедрение этих практик может значительно повысить уровень вашего проекта.
Регистрация
13 марта 14:00
Использование SAST в качестве Quality Gate — это не просто тренд, а необходимость для современных разработчиков, стремящихся создавать надежные и безопасные приложения. Узнайте, как внедрение этих практик может значительно повысить уровень вашего проекта.
Регистрация
Всем привет! Собираемся на IT-завтрак в воскресенье 16 марта в 9:30 в Бруснике на Чистых прудах.
https://yandex.com/maps/-/CDXzzRk8
Кто жаворонки, приходите, посидим, за кружкой кофе обсудим IT-новости Москвы.
По желанию потом можно переместиться в Lion's Head Pub (https://lhpub.ru/).
https://yandex.com/maps/-/CDXzzRk8
Кто жаворонки, приходите, посидим, за кружкой кофе обсудим IT-новости Москвы.
По желанию потом можно переместиться в Lion's Head Pub (https://lhpub.ru/).
TechMeetup #8 👋 Java | JVM x T1 ЛАМПА
День уже длинный, тепло, на улице греет солнышко, природа просыпается, вот и мы тоже решили вылезти из зимней спячки и провести весенний день 17 апреля не только с удовольствием, но и с пользой. Очередной TechMeetup #8 по Java и JVM стеку!
➡️ Если у вас есть идея для доклада и вы готовы выступить — сейчас самое время. Если нужен знак судьбы, то подойдет любой из символов этого сообщения, включая пробелы!
📎 Обращайтесь к @anna_savinovskikh или @SayPoj, если хотите поделиться интересной темой.
💡 Даже если у есть только идея, или вы столкнулись с интересными фактами, но не можете оформить их в доклад, не стесняйтесь писать.
Мы поможем превратить задумку в полноценный доклад и поддержим на всех этапах: от идеи до выступления.
Вот некоторые детали о грядущем митапе:
🗓 Когда: 17 апреля, 19:00
📍 Где: Нижний Новгород
💻 Онлайн: не будет, но будет запись
⭐️ Программа всё ещё формируется, и список докладов будет пополняться. Ждем ваши отклики!
Следите за будущими анонсами, чтобы не пропустить регистрацию.
---
👥 Тоже ждете или у вас возникли вопросы? Присоединяйтесь к нашей уютной группе TechCommon/Java | JVM 👈
Следи за будущими анонсами на основном канале @tech_meetup или тут в @tech_meetup_jv если интересен только JVM стек❤
День уже длинный, тепло, на улице греет солнышко, природа просыпается, вот и мы тоже решили вылезти из зимней спячки и провести весенний день 17 апреля не только с удовольствием, но и с пользой. Очередной TechMeetup #8 по Java и JVM стеку!
Мы поможем превратить задумку в полноценный доклад и поддержим на всех этапах: от идеи до выступления.
Вот некоторые детали о грядущем митапе:
Следите за будущими анонсами, чтобы не пропустить регистрацию.
---
Следи за будущими анонсами на основном канале @tech_meetup или тут в @tech_meetup_jv если интересен только JVM стек
Please open Telegram to view this post
VIEW IN TELEGRAM
XIII IT-конференция «Стачка»
18-19 апреля в Ульяновске соберутся 2500+ IT-специалистов со всей страны: разработчики, маркетологи, дизайнеры, топ-менеджеры и предприниматели.
По промокоду progmsk действует скидка 15% на билет.
250+ докладов по 4 ключевым направлениям в 45 секциях:
• Разработка
• Управление
• Дизайн и контент
• Digital-маркетинг
Выступят спикеры из ведущих компаний, таких как Сбер, Яндекс, Ozon, VK, Альфа-Банк, X5 Digital, МТС Digital, Tilda и др.
Вот некоторые спикеры, которые выступят на «Стачке»:
→ Семён Левенсон, руководитель в Яндекс Маркет. Доклад: «Как я старый сайт на современные рельсы переносил»
→ Александр Туник, руководитель продуктового направления в Рейтинге Рунета. Дебаты на тему: «– Мы можем разработать проект любой сложности для любого заказчика! – Нет, не можете».
→ Митя Осадчук, директор по UX/UI в Сбере. Доклад: «Как объединить ДНК бренда и цифрового продукта».
→ Анна Бочканова, Product owner в Яндекс Метрика. Доклад: «Coming soon: как Яндекс Тег Менеджер упростит разметку событий для рекламы».
Что ещё вас ждет?
→ Нетворкинг-события;
→ Мастермайнды;
→ 2-х часовые мастер-классы от экспертов по направлениям конференции;
→ Экспертная зона — возможность встретиться с профессионалом «один на один».
→ Зажигательное афтепати, чтобы отдохнуть от продуктивного образовательного дня и неформально пообщаться с коллегами.
🚀Специальный гость «Стачки» – Антон Шкаплеров, космонавт-испытатель, четырежды побывавший в космосе.
Антон Шкаплеров – российский космонавт-испытатель отряда ФГБУ «НИИ ЦПК имени Ю. А. Гагарина», Герой Российской Федерации, кандидат технических наук, полковник ВКС России.
Программа, информация о спикерах и билеты доступны на сайте.
НетВоркинг - все на «Стачку»!
18-19 апреля в Ульяновске соберутся 2500+ IT-специалистов со всей страны: разработчики, маркетологи, дизайнеры, топ-менеджеры и предприниматели.
По промокоду progmsk действует скидка 15% на билет.
250+ докладов по 4 ключевым направлениям в 45 секциях:
• Разработка
• Управление
• Дизайн и контент
• Digital-маркетинг
Выступят спикеры из ведущих компаний, таких как Сбер, Яндекс, Ozon, VK, Альфа-Банк, X5 Digital, МТС Digital, Tilda и др.
Вот некоторые спикеры, которые выступят на «Стачке»:
→ Семён Левенсон, руководитель в Яндекс Маркет. Доклад: «Как я старый сайт на современные рельсы переносил»
→ Александр Туник, руководитель продуктового направления в Рейтинге Рунета. Дебаты на тему: «– Мы можем разработать проект любой сложности для любого заказчика! – Нет, не можете».
→ Митя Осадчук, директор по UX/UI в Сбере. Доклад: «Как объединить ДНК бренда и цифрового продукта».
→ Анна Бочканова, Product owner в Яндекс Метрика. Доклад: «Coming soon: как Яндекс Тег Менеджер упростит разметку событий для рекламы».
Что ещё вас ждет?
→ Нетворкинг-события;
→ Мастермайнды;
→ 2-х часовые мастер-классы от экспертов по направлениям конференции;
→ Экспертная зона — возможность встретиться с профессионалом «один на один».
→ Зажигательное афтепати, чтобы отдохнуть от продуктивного образовательного дня и неформально пообщаться с коллегами.
🚀Специальный гость «Стачки» – Антон Шкаплеров, космонавт-испытатель, четырежды побывавший в космосе.
Антон Шкаплеров – российский космонавт-испытатель отряда ФГБУ «НИИ ЦПК имени Ю. А. Гагарина», Герой Российской Федерации, кандидат технических наук, полковник ВКС России.
Программа, информация о спикерах и билеты доступны на сайте.
НетВоркинг - все на «Стачку»!
Введение в Coq: формальные методы и зависимые типы
9 апреля (Ср), 19:00
Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).
Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Первый воркшоп будет посвящён основам программирования на языке Coq.
Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер
✔️либо воспользуйтесь онлайн-IDE
Материалы к воркшопам можно найти в репозитории.
Ждём вас на первом воркшопе в среду 9 апреля в 19:00 на трансляции в YouTube или VK.
В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.
Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.
9 апреля (Ср), 19:00
Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).
Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Первый воркшоп будет посвящён основам программирования на языке Coq.
Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер
✔️либо воспользуйтесь онлайн-IDE
Материалы к воркшопам можно найти в репозитории.
Ждём вас на первом воркшопе в среду 9 апреля в 19:00 на трансляции в YouTube или VK.
В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.
Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.
Forwarded from TechMeetup | Java, JVM
Please open Telegram to view this post
VIEW IN TELEGRAM
Всем привет! Собираемся на IT-завтрак в воскресенье 13 апреля в 9:30 в Бруснике на Чистых прудах.
https://yandex.com/maps/-/CDXzzRk8
Кто жаворонки, приходите, посидим, за кружкой кофе обсудим IT-новости Москвы.
По желанию потом можно переместиться в Lion's Head Pub (https://lhpub.ru/).
https://yandex.com/maps/-/CDXzzRk8
Кто жаворонки, приходите, посидим, за кружкой кофе обсудим IT-новости Москвы.
По желанию потом можно переместиться в Lion's Head Pub (https://lhpub.ru/).
Друзья,
Подготовка к ежегодной 11-й конференции по нагрузочному тестированию (НТ) www.perfconf.ru набирает обороты.
Если вы — инженер или руководитель в области НТ и не просто хотите стать участником, а выступить с докладом и зарекомендовать себя как эксперта, поделиться своим опытом и повлиять на развитие отрасли, то ждем вас — пишите Ирине и вступайте в группу мероприятия https://www.tgoop.com/performanceconf (если знаете таких специалистов — пересылайте им это сообщение).
Темы этого года:
▪️Нагрузочное тестирование
▪️Хаос инженеринг
▪️Оптимизация производительности и тюнинг
▪️Практики DevOps и CI\CD
▪️Управление командой и лидирование
▪️Практики SRE, мониторинга, обеспечение надежности систем, SLO
▪️Разбор реальных кейсов
▪️Тренды индустрии
▪️Использование ИИ для мониторинга, прогнозирования и анализа результатов тестирования
Ждем вас!
Подготовка к ежегодной 11-й конференции по нагрузочному тестированию (НТ) www.perfconf.ru набирает обороты.
Если вы — инженер или руководитель в области НТ и не просто хотите стать участником, а выступить с докладом и зарекомендовать себя как эксперта, поделиться своим опытом и повлиять на развитие отрасли, то ждем вас — пишите Ирине и вступайте в группу мероприятия https://www.tgoop.com/performanceconf (если знаете таких специалистов — пересылайте им это сообщение).
Темы этого года:
▪️Нагрузочное тестирование
▪️Хаос инженеринг
▪️Оптимизация производительности и тюнинг
▪️Практики DevOps и CI\CD
▪️Управление командой и лидирование
▪️Практики SRE, мониторинга, обеспечение надежности систем, SLO
▪️Разбор реальных кейсов
▪️Тренды индустрии
▪️Использование ИИ для мониторинга, прогнозирования и анализа результатов тестирования
Ждем вас!
Введение в Coq: формальные методы и зависимые типы
15 апреля (Вт), 19:00
Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).
Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Второй воркшоп посвящён простым индуктивным типам.
Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE:
https://jscoq.github.io/scratchpad.html
Материалы к воркшопам можно найти в этом репозитории: https://github.com/anton0xf/coq-workshop
Ждём вас на первом воркшопе во вторник 15 апреля в 19:00 на трансляции в YouTube или VK.
В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.
Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.
15 апреля (Вт), 19:00
Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).
Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Второй воркшоп посвящён простым индуктивным типам.
Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE:
https://jscoq.github.io/scratchpad.html
Материалы к воркшопам можно найти в этом репозитории: https://github.com/anton0xf/coq-workshop
Ждём вас на первом воркшопе во вторник 15 апреля в 19:00 на трансляции в YouTube или VK.
В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.
Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.
Введение в Coq: формальные методы и зависимые типы
23 апреля (Ср), 19:00
Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).
Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Третий воркшоп углябит наше понимание индуктивных типов и связанных с ними доказательств.
Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE:
https://jscoq.github.io/scratchpad.html
Материалы к воркшопам можно найти в этом репозитории: https://github.com/anton0xf/coq-workshop
Ждём вас на третьем воркшопе в среду 23 апреля в 19:00 на трансляции в YouTube или VK.
В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.
Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.
23 апреля (Ср), 19:00
Каждый программист знает, что тесты не спасают от ошибок. (Некоторые при этом делают ошибочный вывод, что тесты писать не надо).
Так что, если вы пишите софт, в котором цена ошибки очень высока, тесты кажутся недостаточно надёжной защитой. Что делать программисту, который хочет разрабатывать безупречный код?
Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.
И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.
Третий воркшоп углябит наше понимание индуктивных типов и связанных с ними доказательств.
Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE:
https://jscoq.github.io/scratchpad.html
Материалы к воркшопам можно найти в этом репозитории: https://github.com/anton0xf/coq-workshop
Ждём вас на третьем воркшопе в среду 23 апреля в 19:00 на трансляции в YouTube или VK.
В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.
Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.
Forwarded from Команда T1
Please open Telegram to view this post
VIEW IN TELEGRAM