Введение в Coq: формальные методы и зависимые типы
9 апреля (Ср), 19:00

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

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

Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.

И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.

Первый воркшоп будет посвящён основам программирования на языке Coq.

Если вы хотите участвовать:
✔️установите платформу ROCQ на свой компьютер
✔️либо воспользуйтесь онлайн-IDE

Материалы к воркшопам можно найти в репозитории.

Ждём вас на первом воркшопе в среду 9 апреля в 19:00 на трансляции в YouTube или VK.

В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.

Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.

Всем привет! Собираемся на IT-завтрак в воскресенье 13 апреля в 9:30 в Бруснике на Чистых прудах.

https://yandex.com/maps/-/CDXzzRk8

Кто жаворонки, приходите, посидим, за кружкой кофе обсудим IT-новости Москвы.

По желанию потом можно переместиться в Lion's Head Pub (https://lhpub.ru/).

Друзья,
Подготовка к ежегодной 11-й конференции по нагрузочному тестированию (НТ) www.perfconf.ru набирает обороты.
Если вы — инженер или руководитель в области НТ и не просто хотите стать участником, а выступить с докладом и зарекомендовать себя как эксперта, поделиться своим опытом и повлиять на развитие отрасли, то ждем вас — пишите Ирине и вступайте в группу мероприятия https://news.1rj.ru/str/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. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.

Введение в 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. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.

Введение в Coq: формальные методы и зависимые типы
30 апреля (Ср), 19:00

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

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

Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.

И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.

Четвёртый воркшоп посвятим спискам, деревьям и математической индукции.
Если вы хотите участвовать:

✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE:
https://jscoq.github.io/scratchpad.html

Материалы к воркшопам можно найти в этом репозитории: https://github.com/anton0xf/coq-workshop

Ждём вас на четвёртом воркшопе в среду 30 апреля в 19:00 на трансляции в YouTube или VK.

В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.

Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.

Всем привет! Собираемся на IT-завтрак в воскресенье 4 мая в 9:30 в Бруснике на Чистых прудах. Для веранды всё ещё холодно, поэтому пока сидим внутри.

https://yandex.com/maps/-/CDXzzRk8

Кто жаворонки, приходите, посидим, за кружкой кофе, обсудим IT-новости Москвы.

Я хочу, чтобы про профессию QA-инженера знали так же, как про бухгалтера, врача или учителя.

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

Чтобы на вопрос: «Кем ты работаешь?» можно было с гордостью ответить:

«Я QA-инженер»

— и не добавлять никаких пояснений.

Это отдельная, важная и нужная роль в IT, без которой ни один продукт не выходит в люди. QA-инженер — это тот, кто берёт на себя ответственность за качество.

Это профессия для взрослых. Для внимательных. Для тех, кто умеет задавать вопросы, первым замечать детали и не боится быть тем, кто «не соглашается с первым ответом».

Через 2 дня — я проведу вебинар, который готовила долго.

Собрала туда всё: и боль новичков, и честные ответы, и пошаговый план.

7 мая в 18:00 (по МСК)
Бесплатный вебинар:
«QA-инженер с нуля: как за 3 месяца освоить IT-профессию и выйти на доход от 80 000 ₽»
Если вы хоть раз чувствовали, что хотите перемен, но не знаете, с чего начать — приходите.

📩 Ссылка на регистрацию — >  https://bbschool.ru/vebinar

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

Meetup MskVue.js #13

📍 Москва
⏰ чт, 29 май 2025, 19:00 (+0300)
📺 Трансляция

В 13-ый раз команда сообщества соберет единомышленников и на этот раз в стенах Lamoda Tech!

Вас ждут 3 доклада от опытных спикеров, розыгрыш мерча и просто тонна общения с крутыми разрабами 🙂

Совсем скоро мы представим спикеров в своем сообществе MSK Vue js в ТГ, поэтому самое время вступить, чтобы не пропустить новости митапа 🙂

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


#vue

Подписывайтесь на новые мероприятия в боте @NetworklyBot

Введение в Coq: формальные методы и зависимые типы
12 мая преля (Пн), 19:00

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

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

Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.

И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.

Пятый воркшоп посвятим бинарным деревьям и разберём нетривиальный пример доказательства.
Если вы хотите участвовать:

✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE:
https://jscoq.github.io/scratchpad.html

Материалы к воркшопам можно найти в этом репозитории: https://github.com/anton0xf/coq-workshop

Ждём вас на пятом воркшопе в понедельник 12 мая в 19:00 на трансляции в YouTube или VK.

В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.

Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.

Антиконференция "Summer Merge"

SUMMER MERGE 2025 — та самая летняя айти-тусовка, которую вы ждали. Это место, где соберутся айтишники, чтобы вырваться из рутины и отдохнуть в кругу единомышленников.

Живое общение, свежий воздух, берег Волги, палатка в лесу и никаких клиентов и правок— что ещё нужно, чтобы максимально погрузиться в digital-детокс?

Если вы тоже ужасно устали от офиса или удаленки и мечтаете отвлечься хотя бы на пару дней, тогда встречаемся в эко-парке «Русский берег». Лучше места для чилла на природе просто не найти!

👉 Купить билет со скидкой 10% по промокоду MERGE73

Введение в Coq: формальные методы и зависимые типы
29 мая (Чт), 19:00

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

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

Доказывать правильность своей программы. Однако, доказав корректность алгоритма нельзя автоматически доказать и правильность реализации. Было бы здорово, если бы работающая программа позволяла бы себя верифицировать.

И это в определённой степени возможно. Антон Стеканов с помощью Евгения Каратаева в нескольких воркшопах расскажет об языке программирования Coq, формальных методах и зависимых типах.

Шестой воркшоп посвятим индуктивным пропозициям.
Если вы хотите участвовать:

✔️установите платформу ROCQ на свой компьютер: https://rocq-prover.org/install
✔️либо воспользуйтесь онлайн-IDE:
https://jscoq.github.io/scratchpad.html

Материалы к воркшопам можно найти в этом репозитории: https://github.com/anton0xf/coq-workshop

Ждём вас на шестом воркшопе в четверг 29 мая в 19:00 на трансляции в YouTube или VK.

В организации трансляций нам помогает наш партнёр SBTG.RU. Трансляции в любых конфигурациях под ключ.

Чтобы быть в курсе IT-событий, подпишитесь на телеграм-канал ITMeeting. Это наши друзья, которые анонсируют бесплатные мероприятия в Москве и Онлайне. Здесь вы найдёте и конференции, и митапы, и семинары — форматы на любой вкус. Канал анонсирует и наши встречи. Подписывайтесь.

Для бегунов

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

Для гостей фестиваля

- Живой концерт известных групп: на сцене выступят Найк Борзов, «Отпетые мошенники», «Пропаганда», и «Краски».
- Спортивные площадки: волейбол, бадминтон, йога, фитнес, зумба и т. д.
- Активности от партнеров: игры, мастер-классы, розыгрыши призов и т. д.
- Фудкорт: еда и освежающие напитки будут весь день.

Билеты можно купить на сайте как физическому, так и юридическому лицу: https://runit.digital

BarCode про базы данных

📍 Москва
⏰ ср, 18 июнь 2025, 19:30 (+0300)

На протяжении многих лет, отвечая на вопрос «на чём пишешь?», мы называем разные языки программирования: Go, Java, C#. Считая само собой разумеющимся, что все мы «говорим» и на SQL.

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

✔️ Что такое NewSQL и чем он отличается от NoSQL? Как появилась Пикодата и зачем для этого надо было форкать тарантул? Что Пикодата делает лучше остальных?

Об этом нам расскажет Анатолий Попов, руководитель группы разработки в Пикодате.

Практически двадцать лет взаимодействует с СУБД разного класса — и как пользователь, и как программист, и как администратор. Работал в геймдеве, телекоме, занимался учётными системами.

В Пикодате отвечает за интеграцию c LDAP, форк Редиса, расчёт себестоимости, а также за внедрение Пикодаты к клиентам.

✔️ Трудно ли переехать с базы на базу? А если с нереляционной базы на реляционную? Анна Савиновских, Java-разработчица из Т1, поделится историй переезда с MongoDB на Postgres.

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

🍺 Место встречи — второй этаж Freedom Bar (https://freedombar.ru/), который находится недалеко от ст. м. Дмитровская (4-й выход из метро). Собираемся в среду 18 июня с 19:30 и до упора.


#базы_данных #picodata #mongodb #postgres

Подписывайтесь на новые мероприятия в боте @NetworklyBot