Записки юного ярослэма

Isabelle/HOL: первые шаги Если коротко, Isabelle/HOL - это среда для формальных доказательств, где математика жестко доминирует на кодом. Как начать: 1)Скачиваем с isabelle.in.tum.de 2)Запускаем jEdit, да у изабельки своя собственная IDE 3)Создаём файл с расширением .thy (например, Hello.thy) theory Hello imports Main begin end Имя теории должно совпадать с именем файла. imports Main всегда нужен - он подключает стандартную библиотеку HOL, в которой уже реализована и доказана вся школьная и унив...

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

Собираем истинно НАШ сетап из технологий для проекта. Писать все будем на PHP(да все, никакого js и прочего, только хардкор). В качестве хранения данных используем постгрес, очереди строить будем в базе, кеш нам не нужен(все давно уже на безнале). Сверху полирнем хадупом, на всякий случай. Итого получаем реально НАШ стек разработки Формальная верификация продолжится на некст неделе

Циатата дня - "В тусовке разработчиков всего мира брать опенсорные решения — это зашквар, это делают только тогда, когда не могут создать своё. Тогда берут чужое, но рискуют." Ставь лайк, если тоже шкварился об опенсорс

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

Буквально недвано вышла такая замечательная вещь, как Laravel Boost. Это специальный mcp сервер для умных ии агнетов, который помогает им намного лучше работать с ларкой. Казалось бы, ну помогает и помогает, я и сам могу агенту кастомные правила прописать(которые работают через раз), только то, что под капотом буста это не просто правила, а буквально инсутркции на несколько абзацев, как работать с тем или иным аспектом фреймворка. И работает инструмент мое подчтение. Конкретно я поперхнулся монс...

Нам тут в айтишке обещают конец сытых нулевых. Офк ожидаемо, столько совокупных льгот нет ни в одной отрасли, даже в оборонке Как говорится, не ждём, а готовимся.

Друзья! Чем ближе к завершению Всероссийское голосование за премию Open Source, тем жарче становится финальная борьба за заветное место между главными претендентами на звание лучшего open source решения 2025. PHP уверенно продвигаются в лидеры, стремительно набирая голоса за фреймворки Yii3 и Spiral . Сегодня очень нужна поддержка каждого, кто любит PHP и Yii3. В связи с этим я объявляю масштабный конкурс среди программистов на PHP и всех желающих! Будут разыграны 0 единиц iPhone 17. Условия сам...

Тут недавно вышел yii3. Последний из большой тройки фреймворков, наконец таки обзавелся современной версией. Минимум полтора года всех грели, что вот-вот и 3 версия выйдет в релиз. И вот первая причина, почему мало кто перейдет на 3 версию. Руками выпиливать то гигантское количество Yii::$app, которое есть в коде, мало кто будет. Вторая причина - буквально недописанная документация. Есть как минимум раз, два страницы, в которых тупо нет никакого текста. Причем одна из них это "новая" фича. ...

Тут нежданно и негадоно(нет) "айтишная" виза в США дала скачок в своей цене в 100 раз, и у индусов началась нереальная тряска. Ведь теперь на них всякие гуглы не смогут экономить ФОТ, а значит и работать им будет негде. Внимание вопрос, в какую страну, где, если верить новостям, наблюдается дефицит айтишников, а зп +- устаканились, но все ещё остаются высокими, могут массово поехать кибер-раджи. Тем более что официально по слухам прецедент их найма уже был?