А какая модель писала код? Неужели даже Opus 5 и Fable пишут плохой код? И вот вопрос: Пишут ли они код хуже человека? Может быть, люди пишут такой же код?
Я думаю, что в будущем замечательным путём будет писать код, который можно формально верифицировать. Язык Lean для этого отлично подходит, хотя для него очень мало библиотек. Это печально. Зато можно вайбкодить, давать спецификации кода, а нейросеть сможет их проверить автоматически.
Не знаю, насколько возможно сейчас, но я уверен, что к этому всё может скоро придти.
Добрый день! Сердечно поздравляю вас с таким замечательным успехом! Я сам очень интересуюсь разработкой компиляторов и разработкой ОС.
Думаю, что я готов был бы попробовать поддержать ваш проект, но у меня есть несколько пожеланий по поводу его развития.
Очень прошу не составлять о них первого категоричного мнения, а попробовать беспристрастно разобрать плюсы и минусы.
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, и поделитесь своим мнением.
Думаю, что на работу можно устроиться через знакомых, обращаясь напрямую в компании. Хотя я этого сам не проверял, но такой вариант стоит попробовать.
А какая модель писала код? Неужели даже Opus 5 и Fable пишут плохой код?
И вот вопрос: Пишут ли они код хуже человека? Может быть, люди пишут такой же код?
Я думаю, что в будущем замечательным путём будет писать код, который можно формально верифицировать. Язык Lean для этого отлично подходит, хотя для него очень мало библиотек. Это печально. Зато можно вайбкодить, давать спецификации кода, а нейросеть сможет их проверить автоматически.
Не знаю, насколько возможно сейчас, но я уверен, что к этому всё может скоро придти.
Добрый день!
Сердечно поздравляю вас с таким замечательным успехом!
Я сам очень интересуюсь разработкой компиляторов и разработкой ОС.
Думаю, что я готов был бы попробовать поддержать ваш проект, но у меня есть несколько пожеланий по поводу его развития.
Очень прошу не составлять о них первого категоричного мнения, а попробовать беспристрастно разобрать плюсы и минусы.
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, и поделитесь своим мнением.