https://proofassistants.stackexchange.com/a/940/333

This answer is golden, it links to all of the best materials on Type Theory and related subjects.

https://degoes.net/articles/zio-2.0 🍾

В эту пятницу я буду участвовать в небольшом ивенте «TypeScript. Твой код в опасности» от коммьюнити Vue.js:
https://wearecommunity.io/events/typescript-tvoi-kod-v-opasnosti
Поговорим на тему того, насколько тайпскрипт как язык может гарантировать безопасность исполняемого кода, затронем извечную холиварную в мире JS тему «типы vs. тесты», обсудим различные подводные камни той или иной позиции. Приходите, будет интересно 🙂

Новая версия ресурса для изучения прувера TLA+: https://www.learntla.com
Пост автора о мотивации создания второй версии: https://www.hillelwayne.com/post/learntla

Немного новостей.
1. Я наконец-то навсегда покинул Россию вместе с семьей. Сейчас мы в одном из крупных городов Испании, с нами всё хорошо. Впервые за многие годы я могу вздохнуть спокойно и чувствовать себя в безопасности.
2. Мои статьи на Хабре на русском более недоступны. Все материалы, которые я написал, доступны на английском языке на https://ybogomolov.me и будут только там.

И да, наконец-то я без страха могу написать то, что болело с начала войны:
Нет войне. Нет «русскому миру». Путин и его приближенные — военные преступники, которых должны судить в Гааге. Украïнцi, тримайтеся та борiться, за вами правда! 🇺🇦

Вдогонку к этому списку — упрощенный тайпчекер TypeScript, реализованный только на уровне типов: https://github.com/ronami/HypeScript

Я начинаю выкатывать первую итерацию блогпоста по истории ФП, надеюсь что у кого-нибудь будут какие-то замечания по первой главе
токо осторожно, там до первой главки по истории идет метаисторический выблев на пять экранов
https://gist.github.com/klapaucius/f0adec8a567b7bf000c8bcf99686a9bd

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

Эмоциональный интеллект очень важный навык в нашем изменчивом мире. Его развитие откроет перед вами большое количество новых возможностей.
В четверг, 8 сентября, в 18:00 (UTC +3) я проведу вебинар «Эмоциональный интеллект и зачем он вам нужен». Вместе мы в деталях рассмотрим из чего он состоит и какие выгоды может вам дать его использование.
Трансляция пройдет тут https://youtu.be/XeilTW0vkFI
Присоединяйтесь!

Давно не писал ничего, нужно исправлять ситуацию.
Опубликовал небольшую статью, рассчитанную на новичков, — разъяснение часто встречающихся терминов в среде ФП-разработчиков:
https://ybogomolov.me/fp-jargon-part-1
Это первая статья из небольшого цикла. Кроме того, в работе есть лонгрид (и лонграйт, по правде говоря) на тему корректного и типобезопасного моделирования данных — DDD, make illegal states unrepresentable, тайп-левел, вот это всё. Планирую её до конца квартала всё-таки дописать и опубликовать 🙃
Upd: пересоздал пост, т.к. восстановил комментарии к записям. Пишите, как вам?

В блоге появились комменты! Реализовано это через отличный проект Utterances — они используют механизм GitHub Issues API для ведения комментариев.
Подключайтесь к обсуждениям! ;)

Еще немного тайплевельного программирования — крестики-нолики на типах TypeScript:
https://note89.github.io/typescript-typelevel-tic-tac-toe/

Небольшой апдейт по жизни канала.
Те, кто давно подписан на этот канал, возможно, помнят нерегулярную рубрику #музыкальная_пауза. Я решил, что буду писать про музыку, которая вызывает во мне отклик, в отдельном канале, а этот оставить только для тем, связанных с программированием.
Подписывайтесь: https://t.me/randommusicilike 🤘🏻

Ссылка, которую я теперь буду отправлять всем, кто хочет постигнуть type-level программирование на TS:
https://type-level-typescript.com
Очень круто, рекомендую так же, как и всем уже знакомый репозиторий https://github.com/type-challenges/type-challenges.

https://alexharri.com/blog/build-schema-language-with-infer — отличный пример того, как надо работать с infer.

https://t.me/Loskirs/1195 — статья о складывании чисел на уровне типов. Применен умный алгоритмический трюк, который позволил обойти ограничение на глубину рекурсии, которое возникает при наивной реализации.

Ассемблер на системе типов TypeScript. Во-первых, это красиво. Во-вторых, см. во-первых. Чистое искусство, как по мне: https://judehunter.dev/blog/assembly-interpreter-in-typescripts-type-system

https://busy-beavers.tigyog.app/proofs-about-programs — интерактивное обучение LEAN. Интересно и очень доступно написано.

Подведу небольшие итоги года

За этот год, несмотря на все невзгоды и сложности, я продолжил расти как архитектор и разработчик. Получилось так, что я успешно завершил несколько рабочих проектов, и сейчас работаю в звездной команде вместе с инженерами уровня СТО и Associate Principal. Это дало огромный буст, в первую очередь, софт-скиллам и навыкам управления командами. Отдельно хочу публично поблагодарить мою супругу Арину — без ее коучинговой поддержки такой рост был бы просто невозможен ❤️

В плане программирования 2022 также оказался для меня важным: я продолжил работу над личным брендом и менторской программой по функциональному TypeScript. В первом квартале 2023 планирую запускать первый поток, а пока занимаюсь с несколькими студентами в экспериментальном формате индивидуально. Следите за обновлениями — скоро будет много всего интересного! 🙂

С Новым годом! 🎄

P.S. Также подвел итоги года в своем музыкальном канале. Подписывайтесь 😉