Notice: file_put_contents(): Write of 15160 bytes failed with errno=28 No space left on device in /var/www/tgoop/post.php on line 50

Warning: file_put_contents(): Only 4096 of 19256 bytes written, possibly out of free disk space in /var/www/tgoop/post.php on line 50
Prog.Msk • Channel@progmsk_channel P.281
PROGMSK_CHANNEL Telegram 281
Введение в Coq: формальные методы и зависимые типы
9 апреля (Ср), 19:00

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

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

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

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

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

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

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

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

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

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



tgoop.com/progmsk_channel/281
Create:
Last Update:

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

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

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

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

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

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

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

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

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

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

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

BY Prog.Msk • Channel




Share with your friend now:
tgoop.com/progmsk_channel/281

View MORE
Open in Telegram


Telegram News

Date: |

Just at this time, Bitcoin and the broader crypto market have dropped to new 2022 lows. The Bitcoin price has tanked 10 percent dropping to $20,000. On the other hand, the altcoin space is witnessing even more brutal correction. Bitcoin has dropped nearly 60 percent year-to-date and more than 70 percent since its all-time high in November 2021. Deputy District Judge Peter Hui sentenced computer technician Ng Man-ho on Thursday, a month after the 27-year-old, who ran a Telegram group called SUCK Channel, was found guilty of seven charges of conspiring to incite others to commit illegal acts during the 2019 extradition bill protests and subsequent months. Choose quality over quantity. Remember that one high-quality post is better than five short publications of questionable value. The visual aspect of channels is very critical. In fact, design is the first thing that a potential subscriber pays attention to, even though unconsciously. How to Create a Private or Public Channel on Telegram?
from us


Telegram Prog.Msk • Channel
FROM American