#prog #rust #article

Fish 4.0: The Fish Of Theseus

Довольно подробно описывают различные моменты, возникшие во время переписывания. Советую к прочтению — возможно, портирование далеко не так сложно для вашего проекта, как кажется.

The port wasn’t without challenges, and it did not all go entirely as planned. But overall, it went pretty dang well. We’re now left with a codebase that we like a lot more, that has already gained some features that would have been much more annoying to add with C++, with more on the way, and we did it while creating a separate 3.7 release that also included some cool stuff.

(thanks @teamerlin)

parsing sequences (like dates or version strings) by matching on part index

playground
original example

thanks to @kanashimia for suggesting this one!

#meme про детей

TIL, что GitHub ещё и STL умеет рендерить нынче (у меня 3D-принтера нет, так что я как-то это новшество упустил). Узнал о такой функциональности, решив взглянуть, как выглядит результат генерации этих весёлых ёлочных игрушек: https://github.com/joe-warren/christmas-ornaments/blob/main/haskell-ornament.stl

Мальчик: хвастается перед друзьями новой машиной
Мужчина: хвастается перед друзьями новыми джинсами

#Lean
Многие знают, что после успешно завершённого Liquid Tensor Experiment Кевин Баззард и команда отдохнули немного, и вновь взялись за работу. Они занимаются формализацией доказательства Великой теоремы Ферма.

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

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

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

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

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

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

Похожая история была в XIX веке: Вейерштрасс, Коши, Пеано, Гильберт, все занимались отделением математики от натурфилософии, постановкой её на формальные рельсы. Их критиковали за излишнюю строгость, за изгнание творчества из математики; но, как и в случае с Lean'ом, ответ есть лишь один: если мы занимаемся математикой, хотим быть уверенными в истинности утверждения, всегда иметь опору под ногами, иметь проверяемые универсальные результаты, нужно модернизировать наш средневековый цех всеми доступными современными технологиями. За Lean'ом будущее!

В СМЫСЛЕ НОВЫЙ ГОД НА НОСУ

#meme про... Девушек

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 прям нормальный, выводит типы подвыражений и методы автодополняет :)

ГОВНО С ДЫМОМ

Я нашёл!

В СМЫСЛЕ УЖЕ ЯНВАРЬ