Некоторые обновления HOC: - HVM4 в основном завершен и проходит тестирование. В нем все еще не хватает некоторых важных вещей, но они не срочные, поэтому будут добавлены позже. HVM4 — это, по сути, ультра отполированная версия HVM1, включая все, что мы узнали с тех пор. Теперь я считаю, что подход HVM1 был лучше, чем HVM2 (и Bend), потому что лень действительно важна для оценщиков взаимодействия сети. HVM4 будет основой для Bend2 и SupGen1. - SupGen1 полностью завершен. С момента моих постов в прошлом году не было больших улучшений. Мы можем синтезировать функции, такие как sort(), очень быстро, но композиция все еще медленная. Я считаю, что это можно значительно улучшить для класса сводимых функций, и это позволит создать действительно классные приложения, но требуется больше исследований. Мы надеемся запустить API в следующем месяце. Основное препятствие — кластер, который сейчас мигрирует в более надежное место. Мы сталкиваемся с множеством бразильской бюрократии. Мы не можем много сделать. Если это не очевидно, позвольте мне сказать это вслух: не создавайте технологическую компанию в Бразилии. (: - Bend2 будет запущен немного позже, возможно, через ~2 месяца после SupGen, то есть около мая? Он нацелен на то, чтобы быть языком доказательства, как Lean, но созданным для реальных приложений и кодирования в стиле, а не для математики и статей. Это, возможно, самое непристойное предложение, которое я когда-либо писал, и именно поэтому я думаю, что это будет здорово. Конечно, он все равно будет работать параллельно, как Bend1, с использованием HVM4 в качестве цели. Команда сейчас усердно работает над HVM4 / SupGen. Тем временем я делаю короткий перерыв, чтобы поработать над другим проектом, и вернусь через месяц или около того...