Добрый день! Я пробовал ещё до релиза. Мне нравится гораздо больше, чем VS Code. По дизайну, по тому, как спроектирован интерфейс. Это во многом эмоционально, но всё-таки Zed мне милее, чем VS Code.
Я слышал мнение, что не обязательно делать ставку на резюме. Что современные сайты вакансий мертвы (уверен в этом на 65%). А искать работу нужно через нетворкинг, через знакомых, говоря по русски.
Приветствую! Я тут готовлю заметки для статьи про облегчённые методы оптимизации. Вопрос состоит в том, возможно ли добиться большого прироста производительности, прилагая в разы меньшие усилия. Я думаю, что это в некоторых случаях возможно. По крайней мере, программисту стоит знать базовые приёмы.
Есть три направления оптимизации - оптимизация расхода памяти, оптимизация времени выполнения и оптимизация времени компиляции. Обычно мы приходим к тому, нельзя прибавить одно, не убавив что-то другое.
Меня волнует в первую очередь оптимизация времени выполнения. А вот время компиляции релизных сборок я не прочь как раз увеличить!
Вообще, очень медленная операция в современных компьютерах - это чтение и запись в оперативную памяти. А ввод вывод бывает порой ещё хуже...
По этому очень важно, чтобы ваш код как можно меньше бегал за данными в плашки, и как можно больше работал с данными в кэше процессора (желательно L1) а то и в регистрах.
Вы наверное все знаете, что есть O большое, бывают алгоритмы константные, бывают линейные, логарифмические, квадратичные, экспоненциальные... Обычно, чем меньше O большое, тем быстрее работает алгоритм.
Например, время поиска элемента в хэш-таблице всегда примерно одно и тоже, и не должно меняться в зависимости от того, сколько в ней элементов. А бинарный поиск работает за логарифмическое время.
Казалось бы, хэш-таблица всегда должна выигрывать. Ан нет! O большое позволяет оценить примерную скорость роста затрат по мере увеличения входных данных. Кроме этой оценки есть ещё и коэффициенты. Массив, по которому мы проходимся бинарным поиском может уместиться в кэш, а хэш-таблица нет. Может быть, пока она высчитывает хэш, мы уже десять раз успеем бинарным поиском пройтись по массиву.
Это реальный случай. Кажется, тогда код запускался на микроконтроллере.
Я слышал фразу, что самый главный приём оптимизации - это профилирование. Чтобы что-то оптимизировать, нужно сначала это измерить.
Буду рад, если вы подскажете и другие приёмы.
Где-то ещё я слышал, что оптимизация - это во многом перебор различных приёмов. Вся штука в том, что они друг-друга нивелируют, и нужно подобрать такую комбинацию, которая даст наилучший эффект.
Вообще интересно, что будет, если дать ИИ агентам фрагмент кода, и таблицу способов, как его можно оптимизировать. Пущай перебирает! Небось так можно и глобально оптимальный вариант найти. Главное потом проверить, что он ничего не поломал...
Как жалко, чтоб большинство языков программирования не позволяют доказывать корректность, как мой ненаглядный Lean!
В компиляторах есть такая техника - супероптимизация. Она состоит в том, что мы берём кусочек кода, который хотим оптимизировать, и перебираем все возможные варианты машинного кода, меньшего определённой длины. Так мы ищем самый быстрый фрагмент, про который доказано, что он делает то же, что и исходный код. Ясное дело, что там есть много-много хитростей, чтобы отсечь большую часть невалидных вариантов, но всё равно это работает ужасно медленно.
Обычно супероптимизацию не применяют. Я слышал, её могут использовать, чтобы скомпилировать небольшие кусочки кода, которые потом будет использовать компилятор. Что-то вроде библиотеки оптимизированных фрагментов.
Приветствую! Доказать, что в коде нет багов мешает не только проблема останова, но и Теорема Гробовой Крышки. Она же Теорема Райса. Она утверждает, что если какое-то свойство встречается у одних программ, и не встречается у других, мы не можем для любой из программ доказать, что она обладает этим свойством. Но тут ключевое слово "для любой". Есть куча программ, для которых мы можем доказать очень многие свойства!
Проблема останова разрешима! Пусть и не в общем случае. Но есть даже специальные языки программирования, которые называются тотальными. Если программа на них скомпилировалась, можно быть уверенным: она завершит свою работу.
Один из тотальных языков - это любимый мною Lean. В нём можно доказать, что функция обязательно завершается. А если это так, то Теорема Гробовой Крышки немного ослабляет свои позиции, и мы можем доказывать разные свойства о наших функциях.
Тотальные языки - это очень интересная тема. О ней я выпущу отдельную статью.
Мне очень интересно функциональное программирование. Я сейчас изучаю язык Lean 4. Это функциональный язык программирование и в то же время программа для доказательства теорем. У него есть одна отличная особенность: если на объект не осталось ссылок, и нам нужно создать его копию, объект будет изменён, а не скопирован. Это позволяет сильно повысить эффективность программы.
Но самая интересная особенность - это зависимы типы. Они позволяют выражать любые свойства программы в типах и доказывать их. Мы можем доказать корректность нужной нам программмы, и тогда не нужно будет ни одного теста! Хотя написать доказательство может быть сложнее, чем написать тесты, но зато доказательство практически гарантирует, что ошибок нет! Это всё равно, что написать бесконечное количество тестов!
Думаю, что тесты и доказательства могут идти рука об руку. Тесты используются для поиска багов на этапе разработки, а доказательства пишутся перед крупным релизом, и в первую очередь для критических частей.
Одно омрачает мне радость: язык очень молодой и для него очень мало прикладных библиотек. Гораздо меньше, чем для Haskell.
А вообще я хочу написать про Lean статью. Буду рад, если вы зададите вопросы, а ещё лучше, если попробуете сами попрограммировать на Lean, и поделитесь своим мнением.
Добрый день! Было интересно прочитать про функциональное программирование в реальном мире. Мне нравится идея неизменяемого состояния. Datalog мне симпатичен, хотя я его не использовал.
Один из моих любимых языков на данный момент - это Lean 4. Он такой классный! Там мощнейшая система типов. С зависимыми типами. Она очень выразительная. Одна беда. Библиотек почти нет для прикладного программирования. А ведь этот язык мог бы стать новым Haskell!
Я хорошо отношусь к Clojure, но это язык не моего духа. Я просто не представляю, как можно писать большие программы без статических типов! А ведь в Clojure чаще всего вообще типов не определяют! Никаких вам структур. Только хэш-таблицы. И проверки типов в рантайме. Не представляю, как так можно жить! Это не мой стиль. Мне нравится, когда можно определить все поля заранее, задать их тип, и определить операции над структурой.
Но тут есть одна интересная деталь. У того банка распределённая система. Как они синхронизируют время в своих микросервисах? Я слышал про Логические часы. Их создал Лэмпорт. Они используются для того, чтобы восстанавливать причинно следственные связи.
Скажите, вы что-то слышали про логические часы? Было бы интересно прочитать.
Ура! Я так ждал! Я использовал Gemma 3 12b когда отключали интернет. Вот не знаю, будет ли эта версия лучше, чем предыдущая. С одной стороны, она лучше обучена, а с другой, она сильно меньше.
Хм... Возможно, сложность может уменьшиться, если программист искусен? Например, он может применить хорошие паттерны, а то и вообще монады и моноиды...
Нужно всё-таки признать, что способы чуть-чуть уменьшить сложность всё-таки есть. Языки более высокого уровня могут уменьшить сложность. Использование библиотек позволяет перенести сложность с того, кто пишет продакшен код на автора библиотеки.
Есть хитрые техники, которые сокращают код, если их уметь применять.
Добрый день! Спасибо вам за статью! Я когда-то писал парсер-комбинаторы на Лиспе. Похоже, что подходящей оптимизации не было, комбинаторы работали очень медленно. В языке программирования Lean комбинаторы чуть ли не в стандартную библиотеку встроены. Скажите, может быть, вы не против посмотреть язык Lean, и немного попрограммировать на нём? Он вообще имеет двоякую природу. С одной стороны он язык программирования общего назначения, похожий на Haskell, только там гораздо более мощная система типов - зависимые типы. С другой - средство доказательства теорем. Мне было забавно сегодня доказать теоремы про алгоритм Евклида. Правда, на индуктивном доказательстве я застрял. Но это нормально. Математику я только изучаю.
Вообще мне кажется, что в таких случаях могут помочь программы проверки моделей. Они позволяют смоделировать дизайн программы, и посмотреть, есть ли у него нужные свойства! Может быть, если предварительно написать модель на Alloy (Вот по нему книжка), а потом заставить ИИ работать по этой модели, удастся хоть немного повысить качество?
Вообще, смоделировать программу может быть полезно даже при обычной разработке. Обычно модель получается не очень большой. По крайней мере, гораздо меньше самой программы.
Может быть, тут есть синьёры, которые могли бы проверить этот подход на своих пет-проектах? Мне было бы интересно посмотреть на результат.
Мне вот интересен Lean 4. Это одновременно и язык программирования, и помощник для доказательств. Он помогает изучать математику. Если ты доказал теорему, и верифицировал доказательство в Lean, можно быть практически уверенным, что доказательство правильное.
Ура! Я очень рад тому, что вышла новая Гемма на 12b.
Люблю это семейство моделей. Буду использовать её, когда нет интернета.
Добрый день!
Я очень благодарю вас за эти статьи. Мне они кажутся очень полезными и важными.
Мой вам совет: меняйте картинку на превью, чтобы была какая-то драматургия, чтобы образ развивался от статьи к статье.
Добрый день!
Я пробовал ещё до релиза. Мне нравится гораздо больше, чем VS Code.
По дизайну, по тому, как спроектирован интерфейс.
Это во многом эмоционально, но всё-таки Zed мне милее, чем VS Code.
Добрый день!
Скажите пожалуйста, а каков общий алгоритм оптимизации любой программы?
Может быть, вы знаете книги, в которых его можно посмотреть?
Я слышал мнение, что не обязательно делать ставку на резюме. Что современные сайты вакансий мертвы (уверен в этом на 65%). А искать работу нужно через нетворкинг, через знакомых, говоря по русски.
Вы согласны с этим мнением?
Приветствую!
Я тут готовлю заметки для статьи про облегчённые методы оптимизации.
Вопрос состоит в том, возможно ли добиться большого прироста производительности, прилагая в разы меньшие усилия. Я думаю, что это в некоторых случаях возможно. По крайней мере, программисту стоит знать базовые приёмы.
Есть три направления оптимизации - оптимизация расхода памяти, оптимизация времени выполнения и оптимизация времени компиляции. Обычно мы приходим к тому, нельзя прибавить одно, не убавив что-то другое.
Меня волнует в первую очередь оптимизация времени выполнения. А вот время компиляции релизных сборок я не прочь как раз увеличить!
Вообще, очень медленная операция в современных компьютерах - это чтение и запись в оперативную памяти. А ввод вывод бывает порой ещё хуже...
По этому очень важно, чтобы ваш код как можно меньше бегал за данными в плашки, и как можно больше работал с данными в кэше процессора (желательно L1) а то и в регистрах.
Вы наверное все знаете, что есть O большое, бывают алгоритмы константные, бывают линейные, логарифмические, квадратичные, экспоненциальные...
Обычно, чем меньше O большое, тем быстрее работает алгоритм.
Например, время поиска элемента в хэш-таблице всегда примерно одно и тоже, и не должно меняться в зависимости от того, сколько в ней элементов. А бинарный поиск работает за логарифмическое время.
Казалось бы, хэш-таблица всегда должна выигрывать. Ан нет! O большое позволяет оценить примерную скорость роста затрат по мере увеличения входных данных. Кроме этой оценки есть ещё и коэффициенты. Массив, по которому мы проходимся бинарным поиском может уместиться в кэш, а хэш-таблица нет. Может быть, пока она высчитывает хэш, мы уже десять раз успеем бинарным поиском пройтись по массиву.
Это реальный случай. Кажется, тогда код запускался на микроконтроллере.
Я слышал фразу, что самый главный приём оптимизации - это профилирование. Чтобы что-то оптимизировать, нужно сначала это измерить.
Буду рад, если вы подскажете и другие приёмы.
Где-то ещё я слышал, что оптимизация - это во многом перебор различных приёмов. Вся штука в том, что они друг-друга нивелируют, и нужно подобрать такую комбинацию, которая даст наилучший эффект.
Вообще интересно, что будет, если дать ИИ агентам фрагмент кода, и таблицу способов, как его можно оптимизировать. Пущай перебирает! Небось так можно и глобально оптимальный вариант найти. Главное потом проверить, что он ничего не поломал...
Как жалко, чтоб большинство языков программирования не позволяют доказывать корректность, как мой ненаглядный Lean!
В компиляторах есть такая техника - супероптимизация. Она состоит в том, что мы берём кусочек кода, который хотим оптимизировать, и перебираем все возможные варианты машинного кода, меньшего определённой длины. Так мы ищем самый быстрый фрагмент, про который доказано, что он делает то же, что и исходный код. Ясное дело, что там есть много-много хитростей, чтобы отсечь большую часть невалидных вариантов, но всё равно это работает ужасно медленно.
Обычно супероптимизацию не применяют. Я слышал, её могут использовать, чтобы скомпилировать небольшие кусочки кода, которые потом будет использовать компилятор. Что-то вроде библиотеки оптимизированных фрагментов.
Извините, а как включить турбоквант в LM Studio для Gemma 4 E4B?
Эх... С монадами код был бы краше...
Приветствую!
Доказать, что в коде нет багов мешает не только проблема останова, но и Теорема Гробовой Крышки. Она же Теорема Райса.
Она утверждает, что если какое-то свойство встречается у одних программ, и не встречается у других, мы не можем для любой из программ доказать, что она обладает этим свойством.
Но тут ключевое слово "для любой". Есть куча программ, для которых мы можем доказать очень многие свойства!
Проблема останова разрешима! Пусть и не в общем случае. Но есть даже специальные языки программирования, которые называются тотальными. Если программа на них скомпилировалась, можно быть уверенным: она завершит свою работу.
Один из тотальных языков - это любимый мною Lean. В нём можно доказать, что функция обязательно завершается. А если это так, то Теорема Гробовой Крышки немного ослабляет свои позиции, и мы можем доказывать разные свойства о наших функциях.
Тотальные языки - это очень интересная тема. О ней я выпущу отдельную статью.
Мне очень интересно функциональное программирование.
Я сейчас изучаю язык Lean 4. Это функциональный язык программирование и в то же время программа для доказательства теорем.
У него есть одна отличная особенность: если на объект не осталось ссылок, и нам нужно создать его копию, объект будет изменён, а не скопирован. Это позволяет сильно повысить эффективность программы.
Но самая интересная особенность - это зависимы типы. Они позволяют выражать любые свойства программы в типах и доказывать их. Мы можем доказать корректность нужной нам программмы, и тогда не нужно будет ни одного теста! Хотя написать доказательство может быть сложнее, чем написать тесты, но зато доказательство практически гарантирует, что ошибок нет! Это всё равно, что написать бесконечное количество тестов!
Думаю, что тесты и доказательства могут идти рука об руку. Тесты используются для поиска багов на этапе разработки, а доказательства пишутся перед крупным релизом, и в первую очередь для критических частей.
Одно омрачает мне радость: язык очень молодой и для него очень мало прикладных библиотек. Гораздо меньше, чем для Haskell.
А вообще я хочу написать про Lean статью. Буду рад, если вы зададите вопросы, а ещё лучше, если попробуете сами попрограммировать на Lean, и поделитесь своим мнением.
Добрый день!
Было интересно прочитать про функциональное программирование в реальном мире.
Мне нравится идея неизменяемого состояния.
Datalog мне симпатичен, хотя я его не использовал.
Один из моих любимых языков на данный момент - это Lean 4. Он такой классный! Там мощнейшая система типов. С зависимыми типами. Она очень выразительная. Одна беда. Библиотек почти нет для прикладного программирования. А ведь этот язык мог бы стать новым Haskell!
Я хорошо отношусь к Clojure, но это язык не моего духа. Я просто не представляю, как можно писать большие программы без статических типов! А ведь в Clojure чаще всего вообще типов не определяют! Никаких вам структур. Только хэш-таблицы. И проверки типов в рантайме. Не представляю, как так можно жить! Это не мой стиль. Мне нравится, когда можно определить все поля заранее, задать их тип, и определить операции над структурой.
Но тут есть одна интересная деталь. У того банка распределённая система. Как они синхронизируют время в своих микросервисах? Я слышал про Логические часы. Их создал Лэмпорт. Они используются для того, чтобы восстанавливать причинно следственные связи.
Скажите, вы что-то слышали про логические часы? Было бы интересно прочитать.
Мне тоже очень нравится семейство Gemma. Четвёртая версия показалась мне сравнимой с Gemini 3. Конечно, с поправкой на размер.
Но мне очень интересно провести один эксперимент, для которого у меня нет вычислительных мощностей.
Один человек заметил, что если подобрать и продублировать определённый блок слоёв модели, у неё резко улучшаются показатели.
https://dnhkng.github.io/posts/rys/
https://dnhkng.github.io/posts/rys-ii/
И вот мне интересно, можно ли так улучшить модели серии Gemma 4? Это было бы шикарно!
Вот тред в обсуждении модели: https://huggingface.co/google/gemma-4-31B-it/discussions/60
Буду рад, если кто-нибудь там отпишется.
Ура!
Я так ждал! Я использовал Gemma 3 12b когда отключали интернет. Вот не знаю, будет ли эта версия лучше, чем предыдущая. С одной стороны, она лучше обучена, а с другой, она сильно меньше.
Хм... Возможно, сложность может уменьшиться, если программист искусен? Например, он может применить хорошие паттерны, а то и вообще монады и моноиды...
Нужно всё-таки признать, что способы чуть-чуть уменьшить сложность всё-таки есть.
Языки более высокого уровня могут уменьшить сложность. Использование библиотек позволяет перенести сложность с того, кто пишет продакшен код на автора библиотеки.
Есть хитрые техники, которые сокращают код, если их уметь применять.
Добрый день!
Спасибо вам за статью!
Я когда-то писал парсер-комбинаторы на Лиспе. Похоже, что подходящей оптимизации не было, комбинаторы работали очень медленно.
В языке программирования Lean комбинаторы чуть ли не в стандартную библиотеку встроены.
Скажите, может быть, вы не против посмотреть язык Lean, и немного попрограммировать на нём?
Он вообще имеет двоякую природу. С одной стороны он язык программирования общего назначения, похожий на Haskell, только там гораздо более мощная система типов - зависимые типы.
С другой - средство доказательства теорем. Мне было забавно сегодня доказать теоремы про алгоритм Евклида. Правда, на индуктивном доказательстве я застрял. Но это нормально. Математику я только изучаю.
В любом случае, штука интересная.
Каноническая IDE для Lean - это VSCode. Там работает языковой сервер, который даёт очень много различных подсказок.
Вообще мне кажется, что в таких случаях могут помочь программы проверки моделей. Они позволяют смоделировать дизайн программы, и посмотреть, есть ли у него нужные свойства!
Может быть, если предварительно написать модель на Alloy (Вот по нему книжка), а потом заставить ИИ работать по этой модели, удастся хоть немного повысить качество?
Вообще, смоделировать программу может быть полезно даже при обычной разработке. Обычно модель получается не очень большой. По крайней мере, гораздо меньше самой программы.
Может быть, тут есть синьёры, которые могли бы проверить этот подход на своих пет-проектах? Мне было бы интересно посмотреть на результат.
Мне вот интересен Lean 4. Это одновременно и язык программирования, и помощник для доказательств. Он помогает изучать математику. Если ты доказал теорему, и верифицировал доказательство в Lean, можно быть практически уверенным, что доказательство правильное.
Я для работы с Unicode использую вот эту библиотеку:
https://codeberg.org/atman/zg