Добрый день! Сердечно поздравляю вас с таким замечательным успехом! Я сам очень интересуюсь разработкой компиляторов и разработкой ОС.
Думаю, что я готов был бы попробовать поддержать ваш проект, но у меня есть несколько пожеланий по поводу его развития.
Очень прошу не составлять о них первого категоричного мнения, а попробовать беспристрастно разобрать плюсы и минусы.
1) Очень хотелось бы иметь маркированное объединение с возможностью сопоставления с образцом. Это позволяет гораздо изящнее строить абстракции. Кроме того, я слышал, что прошивки для микроконтроллера часто представляют из себя конечный автомат. А то, что я предложил (алгебраические типы данных) очень хорошо подходят для этого дела.
2) В Java объявить ещё один тип - это достаточно муторное занятие. Нужно создавать отдельный файл, ну и так далее. Но опыт показывает, что полезно создавать не мало больших типов, а много маленьких. А в Java это не удобно.
Я бы хотел, чтобы вы добавили возможность создавать типы в любом лексическом окружении. Это просто сделать, но это очень поможет программистам.
3) Очень хотелось бы, чтобы вы попробовали несколько разных языков: Zig, Lean, Clojure, Prolog если не сделали этого раньше. Это поможет прекрасно расширить кругозор!
4) Не могли бы вы попробовать программу для проверки моделей Alloy model checker? Она позволяет выявлять баги в архитектуре.
Скажите пожалуйста, а почему вы ориентируетесь именно на синтаксис Java, а не на синтаксис Kotlin?
У меня есть ещё много вопросов, но не всё ведь сразу!
Я тут нашёл на GitHub курс по ИИ агентам. Так там говорится, что качество обвязки и ИИ агента влияет на качество результата даже сильнее, чем мощность модели. Слабая модель с качественной обвязкой может оказаться лучше, чем мощная модель с плохой. Я уверен в этом на 90%. Но вот размер этой разницы мне только предстоит выяснить.
Мне вот интересно, какой ваш опыт? Кто-нибудь пробовал вайбкодить сначала по простому, а потом сделать правильную обвязку? Такую, от которой агент стал на голову выше.
Добрый день! Я пробовал ещё до релиза. Мне нравится гораздо больше, чем VS Code. По дизайну, по тому, как спроектирован интерфейс. Это во многом эмоционально, но всё-таки Zed мне милее, чем VS Code.
Я слышал мнение, что не обязательно делать ставку на резюме. Что современные сайты вакансий мертвы (уверен в этом на 65%). А искать работу нужно через нетворкинг, через знакомых, говоря по русски.
Приветствую! Я тут готовлю заметки для статьи про облегчённые методы оптимизации. Вопрос состоит в том, возможно ли добиться большого прироста производительности, прилагая в разы меньшие усилия. Я думаю, что это в некоторых случаях возможно. По крайней мере, программисту стоит знать базовые приёмы.
Есть три направления оптимизации - оптимизация расхода памяти, оптимизация времени выполнения и оптимизация времени компиляции. Обычно мы приходим к тому, нельзя прибавить одно, не убавив что-то другое.
Меня волнует в первую очередь оптимизация времени выполнения. А вот время компиляции релизных сборок я не прочь как раз увеличить!
Вообще, очень медленная операция в современных компьютерах - это чтение и запись в оперативную памяти. А ввод вывод бывает порой ещё хуже...
По этому очень важно, чтобы ваш код как можно меньше бегал за данными в плашки, и как можно больше работал с данными в кэше процессора (желательно L1) а то и в регистрах.
Вы наверное все знаете, что есть O большое, бывают алгоритмы константные, бывают линейные, логарифмические, квадратичные, экспоненциальные... Обычно, чем меньше O большое, тем быстрее работает алгоритм.
Например, время поиска элемента в хэш-таблице всегда примерно одно и тоже, и не должно меняться в зависимости от того, сколько в ней элементов. А бинарный поиск работает за логарифмическое время.
Казалось бы, хэш-таблица всегда должна выигрывать. Ан нет! O большое позволяет оценить примерную скорость роста затрат по мере увеличения входных данных. Кроме этой оценки есть ещё и коэффициенты. Массив, по которому мы проходимся бинарным поиском может уместиться в кэш, а хэш-таблица нет. Может быть, пока она высчитывает хэш, мы уже десять раз успеем бинарным поиском пройтись по массиву.
Это реальный случай. Кажется, тогда код запускался на микроконтроллере.
Я слышал фразу, что самый главный приём оптимизации - это профилирование. Чтобы что-то оптимизировать, нужно сначала это измерить.
Буду рад, если вы подскажете и другие приёмы.
Где-то ещё я слышал, что оптимизация - это во многом перебор различных приёмов. Вся штука в том, что они друг-друга нивелируют, и нужно подобрать такую комбинацию, которая даст наилучший эффект.
Вообще интересно, что будет, если дать ИИ агентам фрагмент кода, и таблицу способов, как его можно оптимизировать. Пущай перебирает! Небось так можно и глобально оптимальный вариант найти. Главное потом проверить, что он ничего не поломал...
Как жалко, чтоб большинство языков программирования не позволяют доказывать корректность, как мой ненаглядный Lean!
В компиляторах есть такая техника - супероптимизация. Она состоит в том, что мы берём кусочек кода, который хотим оптимизировать, и перебираем все возможные варианты машинного кода, меньшего определённой длины. Так мы ищем самый быстрый фрагмент, про который доказано, что он делает то же, что и исходный код. Ясное дело, что там есть много-много хитростей, чтобы отсечь большую часть невалидных вариантов, но всё равно это работает ужасно медленно.
Обычно супероптимизацию не применяют. Я слышал, её могут использовать, чтобы скомпилировать небольшие кусочки кода, которые потом будет использовать компилятор. Что-то вроде библиотеки оптимизированных фрагментов.
Приветствую! Доказать, что в коде нет багов мешает не только проблема останова, но и Теорема Гробовой Крышки. Она же Теорема Райса. Она утверждает, что если какое-то свойство встречается у одних программ, и не встречается у других, мы не можем для любой из программ доказать, что она обладает этим свойством. Но тут ключевое слово "для любой". Есть куча программ, для которых мы можем доказать очень многие свойства!
Проблема останова разрешима! Пусть и не в общем случае. Но есть даже специальные языки программирования, которые называются тотальными. Если программа на них скомпилировалась, можно быть уверенным: она завершит свою работу.
Один из тотальных языков - это любимый мною Lean. В нём можно доказать, что функция обязательно завершается. А если это так, то Теорема Гробовой Крышки немного ослабляет свои позиции, и мы можем доказывать разные свойства о наших функциях.
Тотальные языки - это очень интересная тема. О ней я выпущу отдельную статью.
Мне очень интересно функциональное программирование. Я сейчас изучаю язык Lean 4. Это функциональный язык программирование и в то же время программа для доказательства теорем. У него есть одна отличная особенность: если на объект не осталось ссылок, и нам нужно создать его копию, объект будет изменён, а не скопирован. Это позволяет сильно повысить эффективность программы.
Но самая интересная особенность - это зависимы типы. Они позволяют выражать любые свойства программы в типах и доказывать их. Мы можем доказать корректность нужной нам программмы, и тогда не нужно будет ни одного теста! Хотя написать доказательство может быть сложнее, чем написать тесты, но зато доказательство практически гарантирует, что ошибок нет! Это всё равно, что написать бесконечное количество тестов!
Думаю, что тесты и доказательства могут идти рука об руку. Тесты используются для поиска багов на этапе разработки, а доказательства пишутся перед крупным релизом, и в первую очередь для критических частей.
Одно омрачает мне радость: язык очень молодой и для него очень мало прикладных библиотек. Гораздо меньше, чем для Haskell.
А вообще я хочу написать про Lean статью. Буду рад, если вы зададите вопросы, а ещё лучше, если попробуете сами попрограммировать на Lean, и поделитесь своим мнением.
Добрый день! Было интересно прочитать про функциональное программирование в реальном мире. Мне нравится идея неизменяемого состояния. Datalog мне симпатичен, хотя я его не использовал.
Один из моих любимых языков на данный момент - это Lean 4. Он такой классный! Там мощнейшая система типов. С зависимыми типами. Она очень выразительная. Одна беда. Библиотек почти нет для прикладного программирования. А ведь этот язык мог бы стать новым Haskell!
Я хорошо отношусь к Clojure, но это язык не моего духа. Я просто не представляю, как можно писать большие программы без статических типов! А ведь в Clojure чаще всего вообще типов не определяют! Никаких вам структур. Только хэш-таблицы. И проверки типов в рантайме. Не представляю, как так можно жить! Это не мой стиль. Мне нравится, когда можно определить все поля заранее, задать их тип, и определить операции над структурой.
Но тут есть одна интересная деталь. У того банка распределённая система. Как они синхронизируют время в своих микросервисах? Я слышал про Логические часы. Их создал Лэмпорт. Они используются для того, чтобы восстанавливать причинно следственные связи.
Скажите, вы что-то слышали про логические часы? Было бы интересно прочитать.
Добрый день!
Сердечно поздравляю вас с таким замечательным успехом!
Я сам очень интересуюсь разработкой компиляторов и разработкой ОС.
Думаю, что я готов был бы попробовать поддержать ваш проект, но у меня есть несколько пожеланий по поводу его развития.
Очень прошу не составлять о них первого категоричного мнения, а попробовать беспристрастно разобрать плюсы и минусы.
1) Очень хотелось бы иметь маркированное объединение с возможностью сопоставления с образцом. Это позволяет гораздо изящнее строить абстракции. Кроме того, я слышал, что прошивки для микроконтроллера часто представляют из себя конечный автомат. А то, что я предложил (алгебраические типы данных) очень хорошо подходят для этого дела.
Подробнее можно прочитать вот здесь: https://habr.com/ru/articles/1033910/
2) В Java объявить ещё один тип - это достаточно муторное занятие. Нужно создавать отдельный файл, ну и так далее. Но опыт показывает, что полезно создавать не мало больших типов, а много маленьких. А в Java это не удобно.
Я бы хотел, чтобы вы добавили возможность создавать типы в любом лексическом окружении. Это просто сделать, но это очень поможет программистам.
3) Очень хотелось бы, чтобы вы попробовали несколько разных языков: Zig, Lean, Clojure, Prolog если не сделали этого раньше. Это поможет прекрасно расширить кругозор!
4) Не могли бы вы попробовать программу для проверки моделей Alloy model checker? Она позволяет выявлять баги в архитектуре.
Скажите пожалуйста, а почему вы ориентируетесь именно на синтаксис Java, а не на синтаксис Kotlin?
У меня есть ещё много вопросов, но не всё ведь сразу!
Спасибо вам за вашу разработку!
Добрый день!
Очень ждём статью.
Я тут нашёл на GitHub курс по ИИ агентам. Так там говорится, что качество обвязки и ИИ агента влияет на качество результата даже сильнее, чем мощность модели. Слабая модель с качественной обвязкой может оказаться лучше, чем мощная модель с плохой. Я уверен в этом на 90%. Но вот размер этой разницы мне только предстоит выяснить.
Мне вот интересно, какой ваш опыт? Кто-нибудь пробовал вайбкодить сначала по простому, а потом сделать правильную обвязку? Такую, от которой агент стал на голову выше.
https://github.com/justxor/Harness_ru
Вот тут очень хороший материал.
Здравствуйте! Скажите пожалуйста, а верно ли, что на обработку естественного языка такой подход не масштабируется?
Добрый день!
Четыре года прошло.
Может быть, вы можете всё-таки написать пост?
Да побольше!
Мне будет очень интересно почитать.
Если вам трудно написать всё за раз, попробуйте время от времени писать карточки в Obsidian. Потом можно будет составить статью.
Помнится, я проходил функции только в седьмом классе.
А как это сделать?
Ура! Я очень рад тому, что вышла новая Гемма на 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
Буду рад, если кто-нибудь там отпишется.