"Православный карантин"
слова - Алена Грубер,
музыка - Морок
BABOOSHKA is
Старуха Изергиль - вокал,
Алена Грубер - вокал,
Морок - гитара, вокал,
Владимир Чеповский - барабаны,
Red Raven - бас.

Второй митап про децентрализованый вэб и его экосистему. Андрей Соболь будет рассказывать про CODA Protocol и рекурсивные снарки

Также к обсуждению подключатся Петр Королёв (Matter Labs) Иван Иваницкий (Базовый Блок), Валерий Литвин (Cyber) и Анастасия Кондаурова (MadFish.Solutions) со своими вопросами и комментариями.

Если вы хотите поучаствовать в качестве спикера или эксперта в следующих митапах, смело пишите в телеграм @cybaca

Все материалы Cyber Academy тут:
https://cyber.page/search/Cyber%20Academy

Подписывайтесь на этот канал, а так же на наши соцсети:
https://www.facebook.com/cybermeetups
https://www.instagram.com/cybermeetups

#cyberacademy #decentralizedweb

3-й Moscow Wasm meetup состоится в этот четверг (16 июля) в 19 вечера по мск, регистрация по ссылке:
https://careers.kaspersky.ru/events/webassembly/

Dependent types let us use the same programming language for compile-time and run-time code, and are inching their way towards the mainstream from research languages like Coq, Agda and Idris. Dependent types are useful for programming, but they also unite programming and mathematical proofs, allowing us to use the tools and techniques we know from programming to do math.

The essential beauty of dependent types can sometimes be hard to find under layers of powerful automatic tools. The Little Typer is an upcoming book on dependent types in the tradition of the The Little Schemer that features a tiny dependently typed language called Pie. We will demonstrate a proof in Pie that is also a program.

Come get a taste of Pie, and see for yourself where dependent types can take us.

Speaker: David Christiansen

How do you cope when you can’t choose your own adventure?