Лаборатория Математики и Программирования Сергея Бобровского – Telegram
Лаборатория Математики и Программирования Сергея Бобровского
1.29K subscribers
1.19K photos
24 videos
930 links
ЛаМПовое с Бобровским
Download Telegram
Думаю вот, а тем ли я вообще занимаюсь? ↑↑↑

Программист приходит к гадалке, она ему:
-- Я вижу в вашем будущем много кофе и бессонных ночей...
-- Да это не будущее, это мой обычный спринт!
😁637🤯4🤔3🐳3
ит-работодатели: я открыл вакансию джуниора, и мне за день насыпалось 100500 резюме гы гы гы

ит-сеньоры: я открыл своё резюме, и мне за день насыпалось 100500 вакансий гы гы гы

Хвастанье, что толпа ломится на джуниора -- это просто от безысходности (хотя конечно щёки приходится надувать: дескать у нас такая крутая команда супер-пупер-спецов, просто вот в помощь им набираем; ага ага).

Попробуйте найти даже не сеньора, а хотя бы одного крепкого мидла с норм опытом. Ну или продолжайте пилить проэкты пионерскими дружинами, постепенно раща их в комсомольцы. Их уже ждут в других, более адекватных местах :)
👍52💯133❤‍🔥3🏆1
Сегодня связываться с hr-юшами и рекрутерами становится буквально физически опасно. Они успешо сломали цивилизованный найм более чем полностью, а дальше активно переходят на откровенный скам.

Вам могут дать тестовое задание с "секретным" компонентом без исходников, а когда вы его активируете, ваш компьютер скушает вирус-шифровальщик. Или симпатичная эйчарка разведёт нас на секс крипту. Или вам "гарантируют" помощь и трудоустройство с постоплатой со своей зарплаты, вы найдёте работу на 98% своими усилиями, но потом будете месяцами отдавать до 80% зарплаты. (И не исключено, что вас выгонят достаточно быстро: возможно, это был целиком развод со стороны пары рекрутер-кадровик для распила корпоративного бюджета.)
Или вы будете бесплатно работать "за опыт" над реальными проектами. итд итп.
Это всё реальные неоднократные случаи, на ютубе можете легко найти.

=

Это всё пока было на уровне "физиков", но сейчас растёт ещё одна волна скама -- уже на юридическом уровне. Почему, совершенно понятно: весь этот, мутный кадровый эгрегор:) от низкостатусных рекрутерш до начальников кадровых отделов и топовых техдиров и CTE, работает исключительно в интересах собственников-коммерсантов (чтобы они могли поскорее обновить порш и любовниц). Если например вы трудились программистом в госконторе, то они будут презрительно кривить губы над вашим резюме: "это за опыт мы вообще не щитаем".

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

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

Будьте осторожны и всегда оставляйте за собой немного свободы действий. Возможно, вы действительно не прошли собеседование (и хорошо ещё, что вас при этом ушлые эйчары не развели на деньги).

Но, с другой стороны, всё более вероятно, что на этой вакансии вообще никто не получил и не получит работу…

Будь осторожен. Следи за собой. (с)
46🤔25💯10🙏6🔥4
Такое мы сразу ставим: qutebrowser is a keyboard-focused browser with a minimal GUI. It’s based on Python and Qt and free software.

Однако ключевая его фишка даже не столько клавиатурное управление, сколько "VIM-like browser".

Ньюбы могут предварительно геймифицироваться в теме тут:
vim-adventures.com
47👍7😁7❤‍🔥4🤔2
Я сперва подумал, это прикол такой типа "альтушки для скуфа".
Оказалось, нет.

"C 1 декабря любой гражданин РФ может получить сертификат на бесплатное IT-обучение.
Минцифры приводили статистику о нехватке порядка 700 000 человек в области инновационных технологий. В интересах страны сократить кадровый голод и пополнить резерв новыми специалистами до конца года."

Для этого достаточно пройти вышеупомянутый тест про бабочек в животе например тут:
дефицит-профессий.рф

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

и попросили обязательно указать свой телефончик для круглосуточного спама получения результатов теста...

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

Сама по себе эта активность безусловно полезная, но... не менее странен и её фокус на борьбе с нехваткой 700 тысяч айтишников. Сегодня 1024 резюме приходит на одну вакансию для джуниора, а через полгода такого "бесплатного IT-обучения для всех желающих" на одну вакансию для джуниора просто будет приходить 8192 резюме. Ну и?

Как правильно: вкладывать ресурсы не в неработающую с самого начала госинфоцыганщину, а в трудоустройство. Не в помощь в трудоустройстве! а конкретно в реальное трудоустройство, в создание рабочих мест для начинающих программистов.

=

Но главное: зачем сегодня вообще такие курсы??

Попросите AI (модельки надо брать уровня жпт4o или клода 3.5, окно ставьте 32+)

- написать детальный мета-промпт для создания роадмапа с нуля по обучению в интересующей вас теме в айтишке (например, стать тестировщиком),

- затем скормите ему же этот промпт, получите трек развития,

- попросите его помогать вам на каждом шаге трека, придумывать задачки, проверять ваши решения, подсказывать/помогать итд

-- и он будет (относительно) бесплатно это делать 24/7, причём индивидуально под вас.

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

И в принципе всё.
2😁4329👍182🐳1
Для программиста среда -- это новая пятница!
1😁59👍12💯4
Вот вы говорите "геймдев всё" (регулярно это слышу лет 25 :), огромная конкуренция, даже сеньору устроиться сложнее чем джуну на бэк патамушта каждый школьник мечтает разрабатывать игры, полным полно готовых гейммейкеров без программирования, денех там мало, и вообще невероятно сложно сегодня заработать...

Этой осенью мне предлагали тысячу долларов (но просили чтобы именно я сам делал) за скрипт(!) для хака мобильной игры (нет, не хомяк:): чтобы лут золото бриллианты из сундуков побольше вываливался, чтобы бустить фастпуш и врагов на фраги, чтобы когда с 5лв зашёл такой в кооп, то вышел уже с 25м )))

А главная цель конечно чтобы в итоге всех выносить в pvp и войти в топ рейтинга.

Ну, когда киты донатят сотни тысяч руб в месяц на любовниц свою гильдию, на навороченные скины, на вип-доступ, совершенно не удивлён...

За недельку наверное сделал бы, поюзал anrc , xposed etc, но совсем маловато денежек за такой срок работы дают.
1🤔51👍126🤯2
Вечерние размышления "письмом" )))

Ну блин на дворе третье десятилетие 21 века, но на протяжении 40 лет по-прежнему лучше всего работает дедов принцип

хочешь сделать хорошо -- делай всё сам


Как святые computer science того времени писали САПР-ы с нуля на стековом форте (а это на минуточку посложнее ассемблера будет), так и сегодня приходится им следовать фактически.

1. Сейчас глубоко копаю в learning distillation. Это настолько сложная аналитическая задача, что современные ллм-ки + векторные базки даже и близко темку не вытягивают. Так вот мне под это нужен совсем простой но эээ достаточно специализированный конструктор курсов с максимально простым UI, а те, что я уже сделал для Школы, под эту специфическую задачу не очень подходят.

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

Я пересмотрел несколько десятков доступных конструкторов курсов, ну да, есть 3-4 с минимально удовлетворительными возможностями и rest api. Но до чего же они громоздкие, неудобны и человеконенавистнически в плане UI. Я сам на них регулярно разные курсы прохожу, и в лучшем случае на троечку они тянут.
Поэтому ёлки но опять придётся всё делать самому!..

Контент для одного такого курса у меня в сыром виде на 30% готов -- на тему одного из продуктивных и достаточно известных, но не очень распространённых аджайлов.
Нет, не скрам :) методика достаточно простая, но конкретно заточена на формализацию требований, что классно сегодня ложится на взаимодействие с AI.
1343👍203🔥2🤔1
2. И классическая тема оплаты: хочу сделать эти курсы уже для всех доступными и относительно недорогими, но для этого нужна прозаическая автоматизация приёма оплаты с молниеносный выдачей новых логина пароля к курсу. Да, существующие сервисы по созданию курсов подобное предлагают, ну там во-первых надо полностью завязываться только на них, а во-вторых у них такая мутная интеграция с кассами/эквайрингами, вот реально проще сделать самому. Можно также ставить себе или интегрироваться со всевозможными срм-ками, но всё это возня получается вообще как ужасающий-3.

Ведь так-то я хочу совсем простой мета-сервис: вы принимаете деньги за чей-то курс на свой счёт, сами выдаёте чеки, и переводите на р/с автора например за 10-15% комиссии. И сразу при поступлении оплаты дёргаете пых-скрипт на сайте автора, уведомляя об оплате, сразу получаете от него логин-пароль, показывайте клиенту и шлёте на почту и всё,

Но ничего подобного (в России) ВООБЩЕ нету, Карл!

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

"Я гарантирую, что... никогда не буду ... заключать с кем-то соглашения о партнёрстве (абсолютно всё, от текстовых курсов до программирования учебных сервисов, делаю в одиночку)."

Вот если бы это был чисто автономный сторонний продукт...

=

Однако хорошая новость: я джва дня плотно общался с техподдержкой т-банка (нереклама, блин! искренне пишу), как бы мне такое запилить -- и они прям реально чётко помогли, респект от души, всё получилось!

Но ведь опять такое приходится делать самому...

"Нет школы лучше, чем старая школа" (с) Рок-н-рольщик
2🔥64👍183👏1
Для усиления самомотивации, по вчерашним темам, буду здесь выкладывать прогресс по продвижению к условной Школе 3.0.

1. "Движок".
Архитектура, математика: 42%
Реализация (грузим серию книг по теме и получаем на выходе сырую структуру курса): 30%

2. Фреймворк курса: 0% :)

3. Автоматизация платного доступа к курсам для всех желающих: 23%
Но в первую очередь эти условные курсы 3.0 будут в "раннем доступе" со скидками моим курсантам, и оплатить их можно будет как обычно.

4. Текущий (самый первый) курс: 30%

Буду регулярно отчитываться о продвижении; подозрение однако, что по мере приближения к конечной цели процесс из линейного превратится в логарифмический 😅

/wow (way of the wizard)
Трудно выразить, насколько ценны инженеры, умеющие просто объяснять сложные концепции. А вот если ещё их мышление смоделировать...
149👍31🔥8🤔2🫡2
О продвижении по плану
(100% запланированных задач и 100% незапланированных багов)

1. "Движок". 41%
Архитектура, математика: 42% => 52%
Реализация (грузим серию книг по теме и получаем на выходе сырую структуру курса): 30%

Весьма вероятно что я первый человека в мире кто реализовал гомотопическую теорию типов HoTT на PHP 🫢
PHPoTT )))
А на хаскеле или прувере, так-то любой дурак сумеет.

Пока 900 строк пыха, и потратил где-то около 100 долларов на жпт, а до достаточно полной версии ещё наверное пара сотен уйдёт.
Веб-консоль работает у меня на сайте уже, думаю сделать на её основе игру для обучения вот этому всему (с pvp и донатом, без иронии), ну это пока в далёкой перспективе.

Я запилил сперва λCω (топчик в кубе Барандрегта), но хотт куда мощнее конечно. Сделано: базовый тайпчекер с universes, identity types и пути, j-элиминатор, унивалентность, эквивалентности, гомотопии, n-типы...
Хотел на этом остановиться, но не удержался, выдохнул и за ночь допилил высшие индуктивные типы (HIT) и типы тождества.
Сильно конечно упоролся на фундаменте: вывод типа для терма, затем с уровнями универсумов, потом позабыл технический момент, что коли хочем унивалентность, пути между типами (формальное равенство) всегда должны находиться в следующем универсуме, иначе получается парадокс Рассела, и т.п.

В перспективе будет кубик обязательно (composites, fills) и ещё много чего, но пока хочу закончить БАЗУ PHPoT. Сделано "из запланированного" :) 20%, но процесс на самом деле уже чисто технический. Главное было выгрузить смысл/связки/понимание из учебников HoTT (и моей головы) в ТЗ, чтобы его минимально понял жпт.
Первый курс 3.0 кстати будет как раз о подобном.

Но на самом деле, особо сложного тут нету ничего. Это уровень примерно второго третьего курсов computer science хороших универов из первых десяток мирового рейтинга. Раньше я рекомендовал что тут можно поизучать с околонуля, если вы отучились хотя бы на первом курсе любого инженерного ВУЗа, но потом перестал. Зачем? Лучше я сам вас на этой базе обучу и этой базе, и сильному мышлению в относительно прикладных темках.

Но если прям очень хочется, хоть и не очень понятно а нафига, забустите 50 сердечек, тогда поясню.
Ладно, считаем сердечки + звёзды )
p.s. ну ок) вы красавцы 🙏

В сказке после слов "и жили они долго и счастливо" история заканчивается, а в плане разработки после слов "финальное тестирование" всё только начинается!
❤️❤️❤️❤️❤️
176147🤯10🎉2🔥1
Чем с более сильными программистами вы работаете, тем чётче понимаете, насколько слабый программист вы сами есть на самом деле.

/dev ПРЕКРАТИТЕ использовать Docker Desktop! => OrbStack
it's a supercharged WSL and Docker Desktop alternative, all in one easy-to-use app.
1💯45🔥8🤔6🐳5🤝2
В проектах Теслы основной язык Python, что понятно, т.к. там много ML. Но с другой стороны, а как отлаживать встроенный в машинку зоопарк фреймворков, который по определению надо ещё и регулярно апгрейдить от постоянно находимых багов?

А вот твиттер чистенько кодят преимущественно на Scala.
(elon-musk-has-pulled-more-than-50-tesla-engineers-into-twitter)

/redflag ПРЕКРАТИТЕ использовать print() и log() для отладки питонячьего кода => ic()
data structures are formatted, output is syntax highlighted, includes program context: filename, line number, and parent function...
1🔥47🤔7👏3
Начинаю выкладывать шикарные горячие вакансии, отобранные специально для вас, дорогие 🚀🚀🚀

1. Senior C# Developer в проект по автоматизации цирка

Мы - инновационная компания "ЦифроЦирк", создающая революционные решения для циркового искусства. Наша миссия -- вывести традиционный цирк на новый технологический уровень.

Проект: Разработка системы "CircusOps" - комплексной платформы для управления цирковыми представлениями, включая:
- Калькулятор траекторий для воздушных гимнастов
- AI-система подбора музыки под движения слонов
- Микросервис синхронизации жонглёров
- Биометрический трекер настроения клоунов

Technical Skills (ОБЯЗАТЕЛЬНО):
- C# (.NET Core) - уровень "может написать компилятор с Haskell в IL с закрытыми глазами"
- MS SQL Server - способность оптимизировать запросы быстрее, чем тигр прыгает через огненное кольцо
- Azure Cloud - умение жонглировать микросервисами не хуже профессионального жонглёра
- SignalR - для реалтаймовой координации движений дрессированных медведей на моноциклах
- ML NET - для предсказания вероятности падения акробатов
- React - ваш фронтенд должен быть таким же эффектным, как тройное сальто
- Entity Framework Core - виртуозное владение миграциями баз данных

Soft Skills:
- Стрессоустойчивость уровня укротителя львов
- Умение работать в команде с клоунами
- Способность сохранять серьёзное лицо при обсуждении багов с дрессировщиками
- Креативность фокусника
- Гибкость мышления гимнаста
- Умение жонглировать дедлайнами
- Готовность к внезапным совещаниям на трапеции

Что предлагаем:
- Зарплата: от 99,000 рублей до бесконечности (зависит от количества успешных релизов без падения акробатов)
- ДМС включает страховку от укусов тигров
- Бесплатные билеты в цирк для всей семьи
- Корпоративы с фокусниками и дрессированными пингвинами
1😁61🙏1110👍7🤔4
А что, говорят что где-то на госуслугах надо искать где там зарегистрироваться до 1 января, чтобы получить какую-то "печать блоггера"? У меня было 13т в паблике (сегодня кстати выложил там базу, почему будущее фронтенда за htmx), я поудалял всех собачек и пассивных, осталось почти 10т; решил прямо по живому ещё тыщу обрезать, и потом заморозить на 9,999 папищеков... но по последним постам уже снова до 12т набижали.

Я где-то с конца 1970-х ходил практически на все домашние матчи "Динамо", с самого зарождения фанатского движения бело-голубых в нём участвовал, околофутбол, всё это... Но как появился fan id, только теперь изредка хожу на кубковые матчи.
💯 поддерживаю фэнов не принимать эту "печать фаната" никогда и ни при каких условиях.

Вчера "fan id", сегодня "блоггер id", завтра "666 id"?

=

С другой стороны, а как будут наказывать? Рекламу не разрешат? Так у меня никогда не было её и не будет. Репостить посты запретят? Да и лучше, меньше народу будет ко мне приходить. Донатить не дадут? Но у меня там донатов и нету.

Рассказывают правда, что vk якобы начал рассылать грозные сообщения админам крупных пабликов, что, типа, по вашему сообществу надо обязательно зарегистрироваться "блоггером". При этом совершенно не удивлюсь, если vk, после серии подобных предупреждений, для самостраховки будет за такое просто банить без разбора и возможности восстановления, а соответствующий пункт добавит в пол.соглашение.

Кстати почему бы это не автоматизировать? Если у человека есть верифицированный аккаунт вк, то достаточно дёрнуть один какой-нибудь госAPI с уже известными данными и всё, а админа просто уведомить по факту (если конечно технологический суверенитет действительно работает не на бумаге). Для миддла это 1 день работы (+99 дней бюрократии конечно). Но и этим надо было заниматься заранее, а не постфактум.

Но мне и это пофиг: все материалы паблика сохранены локально, буду их переписывать и выкладывать заново, и при этом следить, чтобы количество подписчиков не превысило магическую цифру 9999.

А может быть, и не буду. Может, заодно и этот канал удалю. Ну мало ли, уеду на Запад следом за математиком Родиным (у него кстати осенью вышел очередной мощный материал "Proclus on Euclid’s definition of plane angle and the concept of mathematical structure according to Voevodsky"), и в России больше не останется ни одного человека, готового обучать HoTT и делать материалы и курсы по этой теме. Или на Восток, послушником в буддийский монастырь, по пути Гротендика. Или на скорости 300+ км/ч случайно последую Болту, D1ablo или Сергею Доренко (в этом по крайней мере есть какая-то эстетика...).

И ничего вы у меня больше прочитать не сможете, хотя и хотели.
1🤔65🫡1710😎105
Обещанное продолжение по HoTT ❤️❤️❤️
Но сперва небольшое отступление.

Ту реализацию гомотопической теории, которую я в основном сделал (осталось поотлаживаться на достаточно сложных примерах), я назвал

ТОП (топологически-ориентированное программирование)
(пока подобного термина нигде не было)

PHPoTT (моя программная реализация ТОП) -- это такой игрушечный функциональный язык с зависимыми типами, который однако умеет мощные штуки: прежде всего это явная работа с гомотопическими путями и высшими индуктивными типами.
Ну, да, нечто подобное по-взрослому умеют кубическая Agda, Arend, Coq с HoTT, Lean... Хотя нет, экспериментальная поддержка HoTT была в Lean 2, начиная с Lean 3 от HoTT отказались в пользу классической математики, а текущий Lean 4 вообще практически полностью сфокусировался на формализации обычной математики.

...В смысле? Разве HoTT -- это не "обычная математика"?
Нет, не обычная )

В "обычной математике" фундамент -- это абстрактная теория множеств, дискретность и статичность, а главное, сами доказательства -- это внешние по отношению к объектам конструкции. А HoTT -- про динамическую природу типов и конструктивные доказательства сами как объекты первого класса.

=

В ряде деталей PHPoTT обходит вышеупомянутые языки и пруверы. Ну например, конечно, тому же языку F* в целом прилично проигрываем, но...
В F* абстрактные refinement types, а у меня конкретные реализации высших индуктивных типов. В F* сложная система эффектов: они там первоклассные сущности в системе типов, и каждая функция должна явно декларировать, какие побочные эффекты она будет "производить" :) Хочешь исключение выбросить? Ставь ручками метку Exn. Надеешься, что чистая тотальная? Ставь Tot. И т.п. А PHPoTT -- простая система с явными гомотопическими путями.

=

Да, но "а что это всё вообще кому-то даст на практике??"

1. Конечно, прежде всего тема формальной верификации -- большое отдельное, которое много лет остаётся дорогим и мало популярным, но... Сегодня в связи с тем, что потихонечку получается получать более-менее рабочий код во всяческих жпт из естественной речи (хотя чем дороже ллмка, тем более (а не менее!) она требовательна к точности и формализмам в словесной заявке), думаю эта тема будет взлетать очень сильно.

2. Когда у нас есть доказуемые изоморфизмы, мы можем верифицировать пути преобразований между всяческими форматами данных например - на уровне математически правильной спецификации для уровня жпт, сформированной автоматически (т.к. HoTT и про гарантированное сохранение свойств при трансформациях).

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

Представляете, когда я обучу вас легко и просто подобным формальным подходам, которые сейчас и близко никто не понимает и не представляет (они даже не знают, что они этого не знают:)? С совершенно конкретным скиллом применения этого в вашей повседневной работе! 💪🏻💪🏻💪🏻💥💥🚀🚀🚀
(если конечно не релоцируюсь:)

Продолжение по курсам 3.0 следует; в следующий раз, как обещал, конкретно про самостоятельное начальное обучение этому напишу (сперва конечно надо в голову встроить соответствующую думательную машинку).

/dev прогресс по курсам 3.0: 23% => 27%
...
2. Фреймворк курса: 0% => 15%
5051👍18🔥5😇1