Лаборатория Математики и Программирования Сергея Бобровского – Telegram
Лаборатория Математики и Программирования Сергея Бобровского
1.29K subscribers
1.19K photos
24 videos
930 links
ЛаМПовое с Бобровским
Download Telegram
...В принципе можно конечно сделать вообще на Лине 4, самое смешное, что поддержка хотт была в третьей версии, но потом её оттуда выпилили, потому что поддержка унивалентности в ядре Lean оказалась пацанам не под силу 😬 Надо переопределять базовые понятия равенства, конфликты с классическими представлениями о тождестве, нарушается UIP и AC, бесконечные иерархии преобразований, запутанные проверки эквивалентности...

Вроде бы тривиально?

def idEquiv {A : Type} : A ≃ A

Да но мы-то хотим такое с унивалентностью в ядре доказательств 🫢
Классическая теория, что с лицом?

Это как попытка встроить квантовую механику в классическую физику: принципиально новый уровень абстракции.

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

1.1. Посмотреть, можно ли на коленке склепать рестик на лине 4.
1.2. Запилить некую минималистичную поддержку хотт.

=

Другой вариант: использовать F* -- микрософт его прям энергично развивает вовсю. И вроде бы это .NET -- но нет )
Сетевой поддержки у него нету, придётся делать обвязки на ocaml, да и сам он позиционируется прежде всего в направлении верификации кода, Lean конечно посильнее в математическом плане.

Поэтому от F* отказываемся, и следующий шаг -- это наш любимый F#. Вот тут в техническом плане сразу всё становится элементарно, но зато мы резко проседаем по системе типов (прежде всего теряем завтипчики) и уже прилично скатываемся на другой конец, ближе к пыхапы 🙈

Навскидку:
HoTT в F#: 7/10 (практически с нуля)
HoTT в Lean 4: 3/10 (почти готовая реализация)

2.1. Если по п.1.1 возникнут явные трудности, когда немного поэкспериментировать с F#.

(размышления продолжаю...)
51🤔42👍112❤‍🔥2🏆1
...Ну и наконец приближаемся ко дну и пробиваем его 😁

Последний минимальный приемлемый язык -- C#.
Теперь у нас уже нету паттерн матчинга "из коробки" и алгебраических типов данных, существенно проигрываем F# как математической нотации, но зато в девятке появились record types, source generators, а так же продвинутые дженерики:
bool IsConnected<U>(HomotopyType<U, IPath<U>> other) where U : IComparable<U>
и даже метапрограммирование:
bool IsHomotopic<T>(this T value, Func<T, bool> predicate)

3. C# хз, ну если только с F# по каким-то совсем конкретным нюансам не получится. В коре на F# эндпоинты вообще в пару строк задаются 😊

[<ApiController>]
[<Route("api/[controller]")>]
type ProofController() =
[<HttpPost>]
member _.ProcessProof([<FromBody>] req: ProofRequest) =
let response = {
Status = true
Result = sprintf "Processed: %s" req.Theorem
}

...
let app = WebApplication.Create()
app.MapGet("/dwarf", fun () -> dwarf)
app.MapPost("/dwarf", fun (dwarf: Dwarf) ->
... Results.Created("/dwarf", dwarf))
app.Run()

=

Посадка на дно начинается с "хотт на питончике" )))
Задаём термы (лямды, универсы, pi-) как датаклассы, а динамическая типизация позволяет вытворять разные штуки на уровне F#.

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

4. MLTT++ на Python по-взрослому (термы/значения как типы данных).

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


5. Ну и в заключение пробиваем дно: пыхапы :)
Ничего не могу сказать, с него я начинал - им же и закончу?
Если получится что-то на питоне, то можно в принципе его код достаточно легко конвертнуть в php...

=

HoTT в Lean 4: 3/10 (почти готовая реализация)
HoTT в F#: 8/10 (практически с нуля, но система типов близка к математической нотации)
HoTT в C#: 9/10
HoTT в Python: 10/10
HoTT в PHP: 12/10

=

В общем, буду пробывать в таком порядке:

4. MLTT++ на Python по-взрослому
1. Lean 4 : REST + HoTT
2. F#
3. C#
4. PHP

Успех предрешён и неминуем.
5238👍12🤯6👌6🫡3
Сам не ожидал, но я всё же завершил свою специальную научную операцию ровно в День Науки! 💥💥💥🚀💪🏻

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

Где-то в 23:50 я успешно прогнал два заключительных базовых теста (унивалентности и "интеграционные":), и только сегодня утром осознал, что намедни уложился таки в святой день! 🤘🙏☺️

Я реализовал БАЗУ HoTT:

1. Базовые типы и зависимые типы
- Реализация Unit, Empty, Sum, Product
- Система Pi- и Sigma-типов
- Механизм зависимых функций

2. Пути и тождества (Path)
- Реализация путей как равенства
- Операции над путями (симметрия, транзитивность)
- Система доказательств для путей

3. Высшие индуктивные типы (HITs)
- Реализация Circle и Torus
- Механизм рекурсии для HITs

4. Унивалентность
- Система эквивалентностей типов
- Транспорт вдоль путей
- Преобразование путей в эквивалентности

5. Бесконечно-группоидная структура
- Реализация путей высших размерностей
- Операции композиции путей
- Механизм когерентности

6. Усечения типов
- Система n-усечений
- Пропозициональное усечение
- Усечение до множества

7. Иерархия универсумов
- Система уровней
- Кумулятивность универсумов
- Полиморфизм по уровням

8. Гомотопические группы
- Вычисление гомотопических групп
- Пространства петель
...

💝💝💝

(продолжение следует)
104❤‍🔥64🫡13👍9🏆6🤝4
This media is not supported in your browser
VIEW IN TELEGRAM
...В мировой микро-тусовке по hott-"программированию" (считанные десятки человек) пишут что-то подобное в основном на хаскеле, ну а я сделал на питончике 🙈

Причём у них там будешь называться реально чётким пацаном, если

a) не просто такое реализуешь, а сделаешь "свой солвер" никому нафиг не нужный , и

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

Впрочем, до этой тусовки мне нет абсолютно никакого дела. Буду продолжать эти темки исключительно на русском, и только в рунете (жаль сайт hott ру занят какой-то попсой :).
Хотя кубик будет обязательно.

так-то я больше склоняюсь к тому, чтобы сделать - по теории типов с нуля до хотт и далее - обучающую гача-игру в духе genshin impact 😬
плавно повышать свой уровень универсума, автоматически получая доступ ко всё более сложным конструкциям.

Хотя нет... В хотт 5+ уровень - это уже наверное на премию Филдса 😇
формализация (∞,1)-топосов, моделирование высших группоидов, бесконечно-категорные структуры...

А в генше вроде до сотого левела можно...

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

(продолжение следует)
137🔥19🫡10👍7🤯1
Ожидание:
HoTT в Lean 4: 3/10 (почти готовая реализация)
HoTT в Python: 10/10

Реальность:
HoTT в Lean 4: 8/10
HoTT в Python: 5/10

Вот этот контринтуитивный момент стал для меня пожалуй самым важным пониманием - из реальной практики - и на него не жалко было потратить несколько сотен долларов. В принципе я как-то интуитивно предполагал:
"...4. MLTT++ на Python по-взрослому (термы/значения как типы данных)."

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

Ровно так и получилось: оказывается что чем сильнее система типов, тем будет не легче а тяжелее реализовывать на ней сложные абстрактные темки. Многие годы до вчерашнего дня я считал 💯 что чем она сильнее, тем в любом случае будет проще и быстрее , при надлежащем уровне понимания, что угодно на ней реализовывать -- но нет.

Теперь совершенно не исключаю что вот именно уровень C# или Python с аннотациями типов и есть как раз тот самый оптимальный баланс относительно реальных прикладных практических задачек которые можно реализовывать с какой-то формальной поддержкой со стороны HoTT.
Буду над этим отдельно много думать, и что с этим пониманием делать дальше.

Конечно моя реализация в некотором смысле игрушечная: type inference "на уровне компиляции" в ней отсутствует по сути более чем полностью, и насколько она потянет конструкции на сотни, а тем более тысячи, термов, вопрос пока открытый. Хотя конечно чисто технически, уверен, это вполне можно будет решить.
Пока всё уместилось в тысячу строк кода, и думаю что теперь уже не будет особых проблем автоматически конвертировать его на PHP или C++. Отдельно хочу попробовать "обратную" схему: из Python-реализации в Lean :)

Ну и буду дальше изучать/экспериментировать с тем что получилось. Ещё вчера я приунывал, что не получится прыгнуть выше MLTT, а сегодня уже думаю, как бы сделать киллер вообще всех систем топового уровня, наподобие lean, f*, agda, coq )))

Потому что у меня всё же цель не продакшен, а обучение этому всему.
1❤‍🔥26🤔227👍71
Продолжаю работу с курсантами 😎

--- GameLogic здесь будут храниться игровые правила и логика управялет тем, КАКИЕ действия будут выполнены
Правильный коммент кстати, как раз сегодня на эту тему я сделал пост.


--- Если после перехода с MySQL на PostgreSQL вся логика хранения пользователей не изменилась — значит, "модель пользователя" была правильной абстракцией, а "таблица в БД" — нет.
---Скрипты, правда, запускаются ощутимо медленнее. Поскольку меня такое раздражает, маловероятно, что буду этим пользоваться.
---Первая серьёзная проблема, с которой столкнулся - установка библиотеки.
---Не начал вовремя, так как отвлекся на заказ секундомера
---Я реализовал СЛИШКОМ много ненужных методов
---поскольку Django Rest Framework в сериалайзерах игнорирует коды при вызове стандартного исключения ValidationError, подставляя всегда 400 статус, то, чтобы не вызывать каждый раз APIException проще сделать собственное исключение
---работаю в рамках одного каталога, хотя нужные мне файлы могут находится и в подкаталогах.
-- Сейчас восстановление возможно только вручную, но планируется автоматизация.
---справедливо будет сказать, что я забыл эти методы исключить после изучения эталонного решения для предыдущего задания

/bdd ...Релизим проект, работаем 24/7, как всегда подвела оценка задачи. Оценивали по форме без анализа внутреннего содержания. Надеюсь когда-нибудь научимся, а пока испытываем боль.
Первый шаг для решения этой классической проблемы -- пройти мой курс по BDD.
35🫡9👍53🤔2
Выложил на бусти первый сериал из 14 материалов СильныхИдей
(уровень понимания крепкий джуниор, но наверняка этим темам вас никто не учил даже в универе :)
Так они доступны только моим курсантам, но тут расширенные версии, дополненные множеством примеров (преимущественно на Java).

Рассматриваем начальную БАЗУ программной инженерии
(правильная форма рассуждений и основы programming in small)
для джуниоров и всех интересующихся:
- три уровня мышления о программе,
- основные принципы снижения сложности кода и повышение его выразительности и понимаемости,
- инженерные подходы к отладке и тестированию.

Формат - html-гайд, в архиве 74 файла, 500 тыс. знаков чистого текста (объём средней книги).
Цена пока 1,999 рублей, через несколько дней повышу.

Бедолагам разрешаю брать "вскладчину" или подождать когда "на торренты сольётся" :)
😁4315🫡9👍21
= Краткое содержание первого сезона =

1. Три уровня рассуждений о программной системе
Вы когда-нибудь задумывались о том, что значит "программа работает неправильно", "программа ошибочна"? Что-то вроде "ну, это когда она вылетает с ошибкой... но если она вроде работает, а может сломаться гипотетически, при определённых условиях... кхм, подождите...".
Давайте разберёмся с этим...

2. Три уровня рассуждений о программной системе - 2
Итак, вы завершили стадию предварительного планирования, и включились в циклы коротких итераций, спринтов, как рекомендует agile. У вас есть доска с множеством листков-задачек, пользовательских требований, которые вам просто надо реализовать. И во всей этой гибкой движухе всё более соблазнительно отказаться от ведения отдельного документа по проектированию...

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

4. Снижение цикломатической сложности кода как метод проектирования (база)

5. Как и зачем избавляться от условного оператора
if-выражения могут создавать экспоненциальное число вариантов работы программы, и вы должны каким-то образом гарантировать, что ваш код успешно работает в каждом из них...

6. О циклах по умному
Каждый раз, когда вы пишете цикл, вы делаете это с одной из нескольких целей. Понимание программы — это искусство восстановления замысла по коду, и тут соответственно будет очень полезен навык быстрого распознавания нескольких разновидностей циклов.

7. Правильное проектирование на микро-уровне
Небольшой, очень наглядный и поучительный пример подходов software design: огромное улучшение, которое мы можем делать даже в крошечных функциях.

8. Три важных принципа programming in small
...Эти три, казалось бы, тривиальных шага помогли и мне, и многим другим, продуктивно выдать много-много качественного кода. Я надеюсь, что они смогут сделать то же самое и для вас.

9. Три свойства качественного кода
Что такое качественный код? На этот вопрос не может быть короткого исчерпывающего ответа. Вопрос "что такое качественный код" сродни вопросу "что такое квантовая физика". Это тема целой области.

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

11. Антипаттерн "Самодокументирующийся код"
Одна из самых странных вещей в программной инженерии -- как много людей ненавидят комментарии. Есть очень авторитетные люди в информатике, которые заявляют, что комментарии -- это признак того, что ваш код плох...

12. Как правильно писать тесты
Действительно, как вы можете добиться прогресса, если тесты всегда срабатывают успешно? Разве вы иногда не делаете ошибки? И что будет, если вы напишете кучу кода, и потом его просто придётся стереть, разве это не обидно, разве это не трата кучи усилий впустую?

13. Как правильно относиться к TDD
Мы учимся с самого начала думать над кодом в терминах спецификации, предметной области, домена: берём техническое задание и транслируем его в формальный вид в виде тестов, которые уже однозначно задают нужную логику поведения.

14. Отладка как наука
Существует ли теория отладки в целом? В основе теории отладки лежит универсальный метод: вы можете ускорить отладку, задавая вот какие вопросы...

Доступен для покупки на бусти.
Формат - html-гайд, в архиве 74 файла, 600 тыс. знаков чистого текста (объём средней книги).
Цена пока 1,999 рублей, через несколько дней повышу.
👍458🤔641
Смотрю, эта вакансия стала мемом, у кого только уже её не видал. Но совершенно никакого возмущения по её поводу не понимаю, хотя недоволен конечно, что тёмный эгрегор эйчаров + хх + хабров + прочих вредителей, безвозвратно сломали русский рынок найма более чем полностью.

Мои курсанты перед тем, как я им порекомендую начинать искать работу и помогать по карьере, сперва должны сделать "дипломный" проект, около 40 заданий. В нём примерно в сравнении с картинкой раз в 10 больше технических темок, которые надо изучить хотя бы с минимальной практикой и продемонстрировать гитхабом, прежде чем рыпаться на поиски juniorской работы.

Тут по большому счёту просто какие-то разрозненные и по смыслу особо не связанные кусочки базы. Основной вопросик, насколько глубоко надо знать каждую из этих тем, а так конечно сегодня это всё фактически must have.

- Докер? Смотрим часовой видосик, и затем пару десятков часов экспериментируем с compose. Главное, суметь на интервью запустить демонстрационный имадж с красивыми окошками (делаем на проекте).

- K8s? Но тут, обратите внимание, требуется не "опыт", а "знание", потому что так-то это отдельная профессия )
Есть Play with Docker, есть Play with Kubernetes, где можно просто из браузера поиграться.

- Настройка CI/CD? Тоже однозначно важная вещь, я курсантам рекомендую, если у них такого на работе (скорее всего) нету, предложить и внедрить как крайне полезное рацпредложение. GitLab CI + Docker изучаются за полдня.
Я вообще всем рекомендую: выполняйте развёртывание как можно чаще (или вашего тимлида пора выгонять).

- Микросервисы? опять требуется не "опыт", а "знания" :)
Ну потому что, будем объективны, джуну вряд ли дадут что-то делать с микросервисами для прода. На второй части дипломного проекта впиливаем обязательно микросервисы с кафкой.

- Spring + Hibernate -- ну это просто по определению базовый фреймворк для Java + базовый ORM (для которого соответственно надо знать стандарт JPA).

- SQL + PostgreSQL - а это вообще фундамент для любой базы бэкенда :)

- gradle/maven - "умные" сборщики пакетов java (на самом деле боль и страдание:), тоже база, без них никуда.

- JUnit - фреймворк тестирования, тут и обсуждать нечего.

- git (из командной строки) - тоже абсолютная база для любого программиста.

Единственное, не очень понял, причём здесь Jupiter (возможно приписали просто по аналогии из-за первой буковки джи :). Это вообще-то темка для питончика и машинного обучения. Ну на гугловском колабе можно пару часов поэкспериментировать, более чем достаточно.

Так что требования к уровню Junior совершенно нормальные, считаю.
(я бы ещё прибавил примерно столько же из computer science :)
В любой инженерной профессии люди обязательно учатся многими годами, прежде чем их подпустят издалека посмотреть на производственный процесс под присмотром бригадира.
С какой стати в программировании должно быть по-другому.

Why the fuck do we let people that have no computer science backgrounds write code? Unacceptable!
444👍154💯1🫡1
Как думаете, на прикладном уровне, так сказать, "кто кого" можно считать подмножеством? Попозже поясню, почему именно так.
Anonymous Quiz
38%
ООП - подмножество ФП
25%
ФП - подмножество ООП
37%
Это непересекающиеся множества
30🤔8👍4❤‍🔥3🔥3
В пояснение вчерашнего опроса ↑ ↑ ↑

Почему именно ФП -- подмножество ООП?
(берём чисто прикладной уровень понимания)

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

2. Алгебраические типы данных из ФП можно реализовать в ООП как "запечатанные" (sealed) классы.

3. Product тип (произведение типов) -- это просто обычный класс.
Sum тип (сумма типов) -- это абстрактный класс, каждый из наследников которого -- один из вариантов sum типа.
Таким образом мы можем комбинировать sum и product типы, создавая иерархии классов, где каждый производный класс представляет конкретный вариант sum типа, а поля класса представляют product типы. А чтобы такая иерархия оставалась "алгебраической", производные классы мы просто запечатываем.

=

В принципе, обратное тоже возможно, но в мэйнстриме будет конечно неприменимо.
Во-первых вообще везде и тотально придётся очень интенсивно использовать HOF (map, filter, reduce, apply, compose...), что подразумевает качественно иной стиль мышления (к счастью современное языки в этом направлении развиваются неплохо).
Во-вторых, инкапсуляцию реализуем через замыкания, наследование через композицию, полиморфизм через дженерики, а абстракции через интерфейсы.

На мой взгляд, стратегически правильный подход -- правильно сбалансированная комбинация этих двух подходов. засада только в том ,что такой баланс не определить без знания cs :)
🤔3714👍94😁1
Сегодня упал хостинг, где я размещаю свои новые курсы (TDD, BDD, лямбда-исчисление... а также курсы для начинающих с нуля).
Собственно единственная причина, по которой я не использую свою собственную прекрасную и неуязвимую обучающую платформу (которую делал сам на 100%), что до сих пор в России нету НИ ОДНОГО автономного сервиса для автоматизации приёма платежей.
Всяческие а- б- в- т- ю- я- кассы, с настройкой которых куча головняка и под которые приходится пилить поверх едва ли не полноценный собственный биллинг, чтобы сделать вообще элементарнейшее: чел оплатил заданную сумму через стандартный интернет-эквайринг, и ему тут же + на почту сбросился ключик доступа или логин пароль, и всё. Я бы за такое и 15% отдавал, но нет. Вот и приходится выкручиваться через всяческие внешние сервисы хостинга курсов, бусти-шмусти, самопальные платёжные боты-фиготы и прочую муть...

Я так понимаю что Selectel -- это же почтовый сервис? Почему тогда весь хостинг курсов упал, ну ладно бы только почта заморозилась. Детский сад штаны на лямках... Сплошные имиджевые потери, не говоря уже о материальных, но PO как правило так и остаются непробиваемыми, сколько им не тверди о важности software design.
Впрочем, совершенно не удивлён, и дальше, по мере роста объёмов кода, безумно ускоряемого "с помощью" AI, будет только хуже.

=

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

"Ключевой вопрос любой зависимости независимо от её типа, очевидно, такой: "Зависит ли А от B?".
Любая зависимость характеризуется как минимум тремя параметрами:
1) семантика или конкретная вычислительная модель,
2) ключевые свойства,
3) пространство допустимых изменений.

"...мой проект включает PostgreSQL в качестве зависимости, но он не зависит от него, если эта база данных не используется, и фактически он и не зависит от него, потому что мой проект не зависит от базы данных..."

В этом высказывании слово "зависеть" используется тремя разными способами. И дело не столько в том, что каждый способ использования "зависеть" -- это ответ на разные вопросы. На самом деле это разные вычислительные исполнительные модели."
🤔41👍14🐳21❤‍🔥1
Завтра на Госуслугах "стартует аттестация айтишников" (или пока приём заявок от потенциальных подрядчиков), и с лета она (по идее) полноценно заработает как Национальная система подтверждения ИТ-компетенций. Не получишь сертификат - ходи голодный :)
В целом одобряю, лучше хотя бы так, чем вообще никак.
(надеюсь это будут не передранные тесты сертификаций оракла и микрософта, или, что ещё хуже, нагенерённые жпт:)

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

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

=

Но пока с нетерпением ожидают завтрашнего утра потенциальные кандидаты на распил тендер очередных миллиардов на госпроект со слабо понятной эффективностью (будет ли такой сертификат давать хотя бы +2% к резюме? очень большие сомнения, если для компаний не будет кнута) ,

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

Сейчас там два набора тестов, постепенно буду добавлять:
Знаете ли вы нововведения C# 9 ?
Знаете ли вы нововведения Spring Framework 6 ?


❤️❤️❤️❤️❤️
527👍6🤔2🔥1
Это хорошо известная сеть платных клиник, обслуживание топчик, врачи супер, к кандидату наук по-любому профилю легко записаться на консультацию за пару дней, а сам приём стоит $30 + доп. процедуры 50-70 долларов, анализы немного подороже конечно. 5 лет к ним хожу регулярно и жутко доволен, в своей реанимации они меня спасли однажды от смерти 🙏😇

За последние годы их стоимость растёт ежегодно примерно на миллиард рублей...
да вот только они экономят лишнюю тыщу долларов на качественном фронтендере )))
Так-то это чисто джуниорский баг: наверняка вместо "name" по невнимательности указали другое поле, какой-нибудь "kind".
Отдел QA? А зачем он нам, и так сойдёт.
фигак фигак и в прод, классика 😬

Курсантам в СИ поясняю контринтуитивную вещь, как автоматизировать тестирование визуальных аспектов (когда в UI что-то пошло не так). Сегодня кстати с помощью AI это значительно проще делать.

На госуслугах планируют тестировать "знание Python, Java, Git...", но зачем, если такие баги - следствие отсутствия малейших признаков грамотно организованного жизненного цикла продукта. Сертификаты надо выдавать прежде всего техдирам, тимлидам, начальникам ИТ-отделов, CTO (это именно их ошибки обходится в сотни/тысячи/миллионы раз дороже программистских), проверять их понимание - как не допускать подобные ошибки,
и без таких сертификатов и близко не подпускать к рабочим процессам.
👍52❤‍🔥1553🤔3
Готовимся к вечеру пятницы: компьютерная версия русской рулетки =>

в баре усаживайтесь всем дримтимом за стол, каждый со своим ноутом, перезапускаете ОС и из чистого списка убиваете случайный процесс (например просто по случайному номеру в списке смотрите pid) ☠️
Выигрывает тот, чей комп ещё будет продолжать работать 🤘
Ставки на победу придумываете сами 🏆

Винда:
taskkill
taskkill /PID 42 /F

Линукс/Мак:
ps -ef
kill -9 42
🤔29😁14🏆14👍3🐳2
На неделе для курсантов добавлены...

...в раздел "Элитный программист" -
59) Почему вам не стоит беспокоиться о составлении идеального плана
Микрозадачи и предварительное планирование нужны только для одного: чтобы свести к минимуму трения в работе. Да, но как это сделать правильно??

...в курс карьеры -
96) Ошибка, незаметно убивающая результаты ваших офферов
Давайте поговорим о критической ошибке, которая незаметно убивает результаты многих ваших офферов: неспособность добиться ...

=

Если вы вдумчиво изучаете и регулярно применяете все без исключения рекомендации моих треков КК, ЭП, БПЗ и СИ+hardwork, без сомнения достигнете 10 программистских совершенств, а также обретёте 37 начал просветления computer science, в числе которых 4 состояния сверхвнимания, 4 сверхспособности и 5 сверхсил.
139👍10💯32🔥2
Консультировал на днях пару команд, моё многолетнее понимание современного мира разработки программного обеспечения стало ещё крепче. Выражается оно одной фразой:
Это просто кучка случайных людей в комнате/в чате, бесконечно спорящих друг с другом...
...и соответственно передающих друг другу в таком формате взаимодействия лишь кривые и ошибочные паттерны софт- и хард-скиллов.

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

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

Но вы думаете , кто-нибудь этому следует? Даже за очень большие деньги? 😁
Они лишь согласно кивают своими собственными головами, на какое-то время глаза загораются "да-да-да"... но через пару дней снова втягиваются в однообразное и рутинное болото разработческой сансары.

Я для начала предлагаю совсем атомарные вещи: например, давайте попробуем просто выполнять деплой почаще, и посмотрим, поможет ли это.

Но мой принцип: никогда ничего не предлагать в лоб. Типа вот я порекомендовал деплой, они так стали делать, и у них что-то улучшилось. Да нифига.

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

Но и то, что я рекомендую потом, уже с учётом многомерности проявившихся проблем, тоже не примитив на уровне "пооптимизировать бизнес-процессы", мои дальнейшие советы -- это уже планы внутри планов внутри планов.
1👍69💯4🤔3❤‍🔥2🤝1
Статически типизированные функциональные языки обладают свойством, которого больше почти нигде нет: если ваша система компилируется, то она обычно и будет работать (почти) как надо с первой попытки. А уж если это система зависимых типов, которая может доказательно гарантировать, что функция делает именно то, что ей и предназначено формальной спецификацией...

Я же говорил тебе, что так уже кодить нельзя
А ты не понимаешь ничего и ничего не хочешь менять
А я учил тебя целый год, тратил время целый год
Ты думала, что я шучу, и до сих пор не можешь понять...
Ты выглядишь так несовременно рядом со мной
.
43👍10🔥10🤔6😁3
Собираюсь на весну-лето подзаработать курьером, на вело.рф смотрю аренду байков яндекса, но при попытке "Узнать адреса" меня посылают куда-то совсем непонятно куда )))

taximeter:// - что это за протокол такой лол

...Понятно, что в каком-то манифесте указано
<data android:scheme="taximeter" />
чтобы прога аренды на мобилке стартовала.

Ну добавьте для браузеров несколько строчек кода, YandexGPT в помощь:

const isMobile = /Android|webOS|iPhone|iPad|iPod|BlackBerry|IEMobile|Opera Mini/i.test(navigator.userAgent);
if (!isMobile) console.log("Not a mobile device");

=

Кстати, html-код лендинга вело.рф, где считанные десятки фраз и одна картинка, занимает 490 Кб, Карл. Первокурсник делал в каком-то визуальном редакторе? )))
Любой жпт нарисует такое за одну минуту и раз в сто компактнее.

А начинается этот код так:

<!DOCTYPE html>
<html class="ua_service_turbo-lpc" lang="ru">
😁589
Рекомендация в варианте яндекс-жпт

const isNotMobile = !(/Android|webOS|iPhone|iPad|iPod|BlackBerry|IEMobile|Opera Mini/i.test(navigator.userAgent));

как-то смутило, а что тут собственно делает ежевичка (ведь давно уже rip)? Я кстати где-то в 2013-м пилил для неё какую-то гиперказуальную игрушку, даже велись переговоры о предустановке её на всех ежевиках в России, но... грянул 2014-й :) и под санкциями они ушли, а потом и по всему миру сдохли. Последствия (с) :)
Но игра несколько сотен долларов успела заработать в конечном итоге. А больше всего на том проекте заработал я: программисты-исполнители всегда в плюсе )))

=

Я проверил жпт, дипсик, алибабу, яндекс, клод, perplexity, и даже хвалёный свежий грок! выставлял вроде везде на "подумать поглубже", смотрел все последние версии, самые дорогие. И это весёлая компания везде выдаёт практически идентичный код - с BlackBerry - с точностью до наименования переменной.
Собственно легко гуглится, что украден он был конкретно отсюда:
https://stackoverflow.com/questions/3514784/how-to-detect-a-mobile-device-using-jquery
Вот как ежевичка влезла: оригинальному посту 14 лет.

=

Гемини, квен и жпт4o затупили, возможно "сами написали" :)
выдали только одну проверку под андроид, даже ифон не добавили.

=

А несомненными победителями нашего рейтинга становятся три брата-близнеца:
жпт 4o мини , лама и гигасбер (который в 20 раз дороже ламы) 😂

if (window.innerWidth > 768) { /* код для десктопа */ }
😁52👍4👏41