Нифига себе:

Narya -- new proof assistant that implements a type theory that is a common generalisation of dTT and HOTT!

Да ещё и написано это чудо на F# OCaml!

(только HOTT это не HoTT :)
This type theory seeks to combine the advantages of "Book HoTT" and cubical HoTT, and avoid some perceived disadvantages of either

Про кубики я пояснял 5 лет назад: "Кубическая теория типов для малышей"

=

"Towards Large Language Models as Copilots for Theorem Proving in Lean"
Our latest experiments show that our co-pilot can automate >80% of the proof steps (2.3 times better than the previous rule-based baseline aesop).

P.S. Тем временем: "Яндекс разрабатывает Календарь+ с ИИ" 😁

Грядёт Java 23 !!1
Поддержка векторных вычислений, паттерн матчинг сделали почётче,
добавили Class-File API (a standard API for parsing, generating, and transforming Java class files), а также Stream Gatherers:
This will allow stream pipelines to transform data in ways that are not easily achievable with the existing built-in intermediate operations.

Только не знаю, "transform data" имеется в виду наверное "pulling data" ?

Вот если "pushing data", было бы реально круто, но скорее всего нет.

... по сути async -- это просто ухудшенная версия зелёных тредов
(бедная java от них отказалась ещё в версии 1.2 :) и так и осталась на уровне C# до явления в нём async/await и Task)
-- только с плохой интеграцией в язык программирования и слабой эргономикой использования.

Однако в большинстве нормальных языков green threads поддерживаются в той или иной форме: Erlang, Go, Haskell, Julia, OCaml, PHP :) , для Python конечно есть расширения, и т.д.

А вот в Rust их нету (но есть async/await и Future), в основном потому, что у Rust нет рантайма, и для встроенной в язык асинхронщины требуется полностью другая механика компиляции + подходящий рантайм, например Tokio (однако в результате легко получить несовместимый в другими рантаймами код :).

Зелёные потоки в основном подразумевают, что компилятор будет вставлять точки выхода везде -- чтобы можно было приостановить выполнение любого потока в любой момент.

=

Короче говоря, в мэйнстриме понимание асинхронщины сводится примерно к такому: "просто сбрось это в тред и забудь о нём". Это самое наихудшее использование потоков, которое только можно себе представить :)

Добавляется сложность и накладные расходы (например, ядрам приходится постоянно кэши сбрасывать). В результате получается, что десятки тредов просто занимаются своими делами, контактируя через какой-то общий объект. Это ужасно и по использованию процессорного времени, и в целом практически всегда это признак плохого проектирования.

Рассказывал подробнее про "concurrency или параллелизм?".

P.S. Вообще, "однопоточный" Rust был бы существенно дружелюбнее и проще. Не исключено, что когда-нибудь это и случится )

Сегодня курсант написал:

...я сломал интеграционные тесты, когда починил, выяснилось, что они были сломаны во многих местах уже и не мной :)

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

Точно по мему! )))

Тонко (и жизненно)

С момента возникновения РФ я был в отпуске два раза: в 1995-м и в 2008-м, когда работал в офисе (и это были самые бесполезные годы в карьере :) просто рутинные задачки без какого-либо роста). За все эти десятилетия я не выезжал за пределы МО (за исключением 2013-го, когда ездил по приглашению в Питер, в гости к Олегу Степанову, CEO JetBrains на тот момент).

У меня нету и не было автомобиля (но есть мотоцикл и 5 велосипедов:). Дачи нету, домик у жены в Солнечногорске. Я живу очень скромно, кушаю простую пищу, ношу неубиваемую спортивную одежду, и мне особо ничего не нужно и не интересно, кроме computer science и роста моих курсантов (по зарплате :).

Я практически никогда не отдыхаю, да и не люблю "отдых", у меня за 45 лет карьеры программистом ни разу не бывало выгорания или приступов прокрастинации
(на треке "Элитный программист" начал выкладывать материалы, как с ней справляться, первый материал "Тайные техники монахов, лучших спортсменов и элитных военных"),
и прекрасно себя чувствую.

Чего и вам искренне желаю! :)

Ну, кто хочет сегодня поработать? :)

Вышел pre-release Torch Titan (a native PyTorch Library for large model training).

Currently we showcase pre-training Llama 3 and Llama 2 LLMs of various sizes from scratch.
Get started in minutes, not hours!

Отлично дополнит мой курс по PyTorch.

В Москву приехал первый Tesla Cybertruck.

v0.dev — киллер реакта? )))

Generate UI with shadcn/ui from simple text prompts and images.

VK, Сбер и Яндекс не смогли договориться о распиле многосотмиллиардного бюджета создании консорциума для разработки общей российской мобильной операционной системы (ОС) на основе Android.

Я кстати предлагал за миллион рублей и пару дней "создать" русифицированную пользовательскую мобильную ОС с поддержкой Android-приложений на базе открытой платформы AOSP.

Те же люди, которые говорили, что ты занимаешься никому не нужной фигнёй и это пустая трата времени, спустя пару дней спрашивают "а как ты это сделал??" :)

Ну, с Днём Шифровальщика! :)

Чем сегодня можно позаниматься в этих темках? Например попробовать сломать какой-нибудь децентрализованный консенсус, накупив побольше стеков :)

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

Пацаны из opengames например построили свою теорию по блокчейнам для игр, сделали солвер для формальных доказательств корректности, и нехило зарабатывают консалтингом по таким консенсусам. И спрос на их услуги будет только расти -- по причине из предыдущего абзаца.

Это из скриптов TON - The Open Network.

Зачем добавляется каталог верхнего уровня в список путей поиска модулей? Зачем путаница с именованием path и dir? Всё мутно и неочевидно.

И вы после моих курсов ещё сомневаетесь, сможете ли стать вот таким элитным программистом, вот такого мирового уровня? Сможете ли работать у Дурова например?

Одна из множества прекрасных идей для клонирования: Wellness for Busy People.

После того, как, к счастью, нельзя стало расплачиваться картами онлайн за это всё (и, надеюсь, хотя бы ещё лет 10 так продолжится), в России стремительно растёт огромный рынок национальных аналогов (в том смысле, что он совсем пустой:). Я подписан уже на несколько десятков бусти/шмусти и других платных русских подписок, и очень доволен, но хотелось бы гораздо большего.

С удовольствием бы платил 500 рублей в месяц и за клон подобного сервиса производственной гимнастики (2000+ разминок и растяжек на рабочем месте).

"Our AI adapts to your team's habits, suggesting health breaks at the most opportune times."

Вот ещё идея для клонирования: "The official Atomic Habits app", тысячи их!

Главное, не надо бросаться "вкладываться" в разработку; максимум за пару недель запилите MVP (прочитайте сперва с курса карьеры "Как правильно создавать
прототип/MVP вашего продукта,и надо ли это вообще делать?"), сделайте лендинг или группу вк, дайте тестовую рекламу на 1000 рублей и посмотрите, какой будет интерес. Если получится конверсия 1-2% в лиды, значит дело стоит того.

То странное чувство, когда заходишь через впн на сайт ФБР :)

То, что в ООП (и ранее) называется "модульностью", и то, что в ФП сейчас называется "композиционностью", на самом деле одно и то же: возможность комбинировать сущности на основе их интерфейса/типа без необходимости программистам одной из таких сущностей заглядывать внутрь другой.

Но есть нюанс: в мае раза три уже, в чатах, в отчётах hard work ребята писали, как постоянно путаются с интерфейсами, абстракциями и контрактами. Я как раз готовил большой материал для СильныхИдей (позавчера выложил), думал, что он будет довольно теоретическим, однако внезапно оказалось, что он реально востребован! В нём я рассмотрел случай, когда множества интерфейсов и абстракций не пересекаются, а дальше теперь поясню ситуацию их пересечения.