1.84K subscribers
3.26K photos
129 videos
15 files
3.54K links
Блог со звёздочкой.

Много репостов, немножко программирования.

Небольшое прикольное комьюнити: @decltype_chat_ptr_t
Автор: @insert_reference_here
Download Telegram
Forwarded from brain_leakage_etc
TIL, что GitHub ещё и STL умеет рендерить нынче (у меня 3D-принтера нет, так что я как-то это новшество упустил). Узнал о такой функциональности, решив взглянуть, как выглядит результат генерации этих весёлых ёлочных игрушек: https://github.com/joe-warren/christmas-ornaments/blob/main/haskell-ornament.stl
11
Мальчик: хвастается перед друзьями новой машиной
Мужчина: хвастается перед друзьями новыми джинсами
🌚12👍5
Блог*
💅
💅
💅9🤮3🤡32💩2👍1
Блог*
💅
💅3116🤡9💩7🤮6👍2👌2🔥1😍1
Forwarded from Матразнобой (Altan)
#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.

В своём блоге Кевин рассказал об их продвижениях до сих пор. И это совершенно прекрасная история, написанная живым и слегка ироническим языком.

Кратко, его товарищи в процессе работы, прописывая основания кристальных когомологий, обнаружили, что оригинальное доказательство не компилируется. В нём нашлась неустранимая дыра: доказательство ссылается на статью N.Roby 1965 года, Лемма 8 из которой неверна. Что удивительно, N.Roby доказывает её, неправильно цитируя свою же статью 1963 года.

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

Кевин, чем писать электронные письма экспертам, выпил кофе с одним профессором, пообедал с другим, и в конце концов нашёлся текст Артура Огуса, который закрывал дыру, а сам Артур взялся закрывать известные ему дыры в этом своём тексте.

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

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

Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!
🔥22❤‍🔥5👍3
В СМЫСЛЕ НОВЫЙ ГОД НА НОСУ
🌚7🤔4👍1
#meme про... Девушек
💅32🙏9😱4🤡4🤣41
Forwarded from brain_leakage_etc
jshell> Stream.iterate(1, x -> x * 4 + 1).limit(10).map(Integer::toBinaryString).map(x -> " ".repeat(9 - x.length() / 2) + x).forEach(System.out::println)
1
101
10101
1010101
101010101
10101010101
1010101010101
101010101010101
10101010101010101
1010101010101010101


С Наступающим!

BTW, jshell прям нормальный, выводит типы подвыражений и методы автодополняет :)
🎉17🤡21
ГОВНО С ДЫМОМ
19💩4🤡4🎉2💯1🖕1
Я нашёл!
9🥴6😁2
Forwarded from Блог*
👍5
Forwarded from Блог*
Блог*
Photo
🍌4
В СМЫСЛЕ УЖЕ ЯНВАРЬ
😁14🤡4🖕21😭1
#prog #article

Debugging memory corruption: Who wrote ‘2’ into my stack?!

Статья из 2016 про отладку связанного с сокетами кода Unity на Windows.

TL;DR: в коде Unity для обработки очереди сокетов использовался сисколл select, в реализации которого вызывалась функция, которая записывала статус возврата в переменную на стеке. При добавлении нового сокета нужно было прервать исполнение сисколла, чтобы можно было начать слежение за состоянием нового сокета. В реализации на тот момент использовалось API для добавления пользовательских асинхронных коллбеков на состояния потока. Этот коллбек выбрасывал исключение, что приводило к раскрутке стека. Когда выполнение сисколла завершалось, он записывал статус в стековую переменную, которой больше не было.
👍6🤯5😱2
Forwarded from someone's shitpost (devilreef)
7👍7❤‍🔥1🥰1
Блог*
Документация Go: "Go — простой язык, в нём есть только один цикл: for". Тем временем for: - Безусловный цикл - Цикл с предусловием - Цикл в стиле C - Цикл по слайсу - Цикл по строке - Цикл по мапе - Цикл по каналу
cat >> go_loops.txt <<EOF
- Цикл по числу
- Цикл по функции, принимающей коллбек с нулём аргументов
- Цикл по функции, принимающей коллбек с одним аргументом
- Цикл по функции, принимающей коллбек с двумя аргументами
EOF
4🤮4😐1
#video #music

Не могу перестать смотреть, это смешно (и не очень далеко от реальных игр D&D)

youtu.be/8HqLysSnnlQ
3
MILF: Miss I would Like to Fondle
🥰2👎1
Статический анализ GitHub Actions

Сразу после релиза новой версии линтера, я задался вопросом обновления своего шаблона для создания новых питоновских библиотек: https://github.com/wemake-services/wemake-python-package

И я понял, что я несколько отстал в вопросе стат анализа GitHub Actions и прочей инфраструктуры.
Расскажу о своих находках.

pre-commit ci

Все знают про пакет pre-commit? Несколько лет назад он получил еще и свой собственный CI, который умеет запускаться без дополнительного конфига. И автоматически пушить вам в ветку любые изменения. Что супер удобно для всяких ruff / black / isort и прочего. У нас такое стоит в большом количестве проектов. Вот пример из typeshed. Вот что поменялось автоматически.

Строить CI на базе pre-commit очень удобно, потому что тебе просто нужно скопировать пару строк в конфиг. А плюсов много:
- Автоматически исправляются многие проблемы
- Автоматически запускается CI, 0 настроек
- Локально все тоже работает одной командой: pre-commit run TASK_ID -a

actionlint

Первый раз я увидел actionlint внутри CPython и затащил его в mypy. Actionlint на #go, он предлагает набор проверок для ваших GitHub Actions от безопасности до валидации спеки вашего yml. Довольно полезно, позволяет найти много мест для улучшений.


test.yaml:3:5: unexpected key "branch" for "push" section. expected one of "branches", ..., "workflows" [syntax-check]
|
3 | branch: main
| ^~~~~~~
test.yaml:10:28: label "linux-latest" is unknown. available labels are "macos-latest", ..., "windows". if it is a custom label for self-hosted runner, set list of labels in actionlint.yaml config file [runner-label]
|
10 | os: [macos-latest, linux-latest]
| ^~~~~~~~~~~~~
test.yaml:13:41: "github.event.head_commit.iss.onessage" is potentially untrusted. avoid using it directly in inline scripts. instead, pass it through an environment variable. see https://docs.github.com/en/actions/security-for-github-actions/security-guides/security-hardening-for-github-actions for more details [expression]
|
13 | - run: echo "Checking commit '${{ github.event.head_commit.iss.onessage }}'"
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~


Даже умеет автоматом shellcheck запускать на ваши run: скрипты!

zizmor

Исходники. Уже на #rust, он более злой. Делает похожие вещи: находит проблемы безопасности. Находит много проблем.

Вот пример, сколько всего он нашел в mypy.


warning[artipacked]: credential persistence through GitHub Actions artifacts
--> mypy/.github/workflows/mypy_primer.yml:37:9
|
37 | - uses: actions/checkout@v4
| _________-
38 | | with:
39 | | path: mypy_to_test
40 | | fetch-depth: 0
| |________________________- does not set persist-credentials: false
|
= note: audit confidence → Low

error[dangerous-triggers]: use of fundamentally insecure workflow trigger
--> mypy/.github/workflows/mypy_primer_comment.yml:3:1
|
3 | / on:
4 | | workflow_run:
... |
7 | | types:
8 | | - completed
| |_________________^ workflow_run is almost always used insecurely
|
= note: audit confidence → Medium


check-jsonschema

Еще есть вот такой проект, он в основном полезен за счет доп интеграций: можно проверять dependabot.yml, renovate.yml, readthedocs.yml и многое другое.

Ставится просто как:


- repo: https://github.com/python-jsonschema/check-jsonschema
rev: 0.30.0
hooks:
- id: check-dependabot
- id: check-github-workflows


Выводы

Как всегда – статический анализ многому меня научил. Я узнал много нового про безопасность GitHub Actions, про вектора атаки, про лучшие практики. А сколько проблем в ваших actions?

Скоро ждите весь новый тулинг в python шаблоне v2025 😎
🔥12