https://verynormal.io

An Obsidian KB on #statistics in general and biostatistics specifically.

Sadly, https://en.wikipedia.org/wiki/Michael_Madsen passed away yesterday July 3, (reportedly) from cardiac arrest at the age of 67. RIP. 😞

Парадокс кошки.

Чтобы отвлечь кошку от деструктивных действий, приходится давать ей всё более сложные игрушки-головоломки. Это приводит к развитию мышления, что ведёт к ещё более деструктивным действиям.

Mario Carneiro is (slowly) proving the Lean 4 (kernel) correct in the Lean 4 itself:
https://www.youtube.com/watch?v=hAj81bYngDA

There are curious insights into Lean 4 metatheory and actual implementation.

https://www.youtube.com/shorts/cZB_OD5qCHo

A gentleman walking (and swimming) across most of the world, save for Antarctica, Australia and Africa. Still a lot of ground (and quite a bit of water and ice) to cover. 🤯

https://blog.sshh.io/p/how-to-backdoor-large-language-models

Turns out fine-tuning a LLM to secretly insert backdoors is pretty cheap and easy. Another twist on trusting trust. Don't trust LLMs you didn't train yourself. Like you don't use compilers provided be a third-party. 😏

https://www.minimax.io/news/minimaxm1

Another Open-Source Open Weights (456B) LLM, this time from Singapore.

Other twists include
— 1 million input tokens and 80k output tokens (that's a lot)
— a new reinforcement learning algorithm: CISPO
— a hybrid-attention mechanism incorporating Lightning Attention

Benchmarks look pretty impressive. 😁

Книжку Григория Сапунова про JAX переводят на русский язык:
https://dmkpress.com/catalog/computer/data/978-5-93700-192-4/

Оригинал издан Manning:
https://www.manning.com/books/deep-learning-with-jax

Сапунов теперь, видимо, больше всего знаменит своим каналом @gonzo_ML — что полностью заслужено, канал отличный: интересный и познавательный. В прошлом, видимо, был знаменит своей работой в Яндекс.

JAX знаменит своим JIT, Automatic Differentiation и поддержкой Google TPU. И там ещё всякого разного вокруг накрутили.

В общем, интересная штука.

STOP DOING CATEGORY THEORY

https://arxiv.org/abs/2404.16321

Pattern runs on matter: The free monad monad as a module over the cofree comonad comonad

Statement dreamed up by the utterly deranged
🥴

Лучше брускетта на фокачче, чем факап на факапе!

https://lawrencecpaulson.github.io/2025/07/02/Finish_your_degree.html

Paulson's take on billionaires and PhDs. 😁

“Relative Toposes for Artificial General Intelligence„ slides.
Part 1 and Part 2.

Hmmm... 🤔

The International Conference on Formal Structures for Computation and Deduction (FSCD) will be streamed online via Zoom for free Tuesday 15 - Friday 18 July, 2025. You can register here:
https://fscd2025.github.io/

🥦 Broccoli Programming

BroccoliController.java

@RestController
@RequestMapping("/broccoli")
@RequiredArgsConstructor
public class BroccoliController {
  private final BroccoliService broccoliService;
  private final BroccoliMapper mapper;

  @GetMapping("/get_some")
  public BroccoliDTO getSome() {
    return mapper.toDTO(broccoliService.getSome());
  }
}

BroccoliService.java

@Service
@RequiredArgsConstructor
public class BroccoliService {
  private final BroccoliRepository  broccoliRepository;

  public Broccoli getSome() {
    return broccoliRepository.getSome();
  }
}

BroccoliRepository.java

@Repository
@RequiredArgsConstructor
public BroccoliRepository {
  private final JdbcTemplate jdbcTemplate;

  public Broccoli getSome() {
    return jdbcTemplate.query(...);
  }
}

> требуется работница с сознанием компьютера
Вы находитесь здесь
> требуется компьютер с сознанием работницы
> требуется работница с сознанием компьютера

I'm still waiting for when they start employing LLMs to forecast the weather. I want to read forecasts I like, and not this crap of a weather!

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

ДМК Пресс перевели ещё одну книжку про компиляторы для начинающих:
https://dmkpress.com/catalog/computer/programming/978-5-93700-391-1/
Х. Мёссенбёк "Конструирование Компиляторов"

В девичестве "Compiler Construction": https://ssw.jku.at/CompilerBook/

Книжка про компиляторы — это хорошо, что плохо — из 8 глав 5 рассказывают про синтаксический разбор, и ещё одна — просто введение. Т.е. только две главы посвящены "мясу" компиляции: семантическому анализу и генерации кода. Для главы про оптимизации места не нашлось, к сожалению. При этом генерация кода рассматривается для стековой виртуальной машины, поэтому распределение регистров, выбор и скедулинг инструкций остались за бортом. Семантический анализ глубиной и широтой охвата похвастаться тоже не может.

Но в плюсе наличествует предисловие от Никлауса Вирта, глава про атрибутные грамматики и большое количество упражнений.

#compiler #book

If you were thinking about visiting Romania in mid-September, you can crash The Working Formal Methods Symposium as well:
https://fromsymposium.github.io/
September 17-19, Alexandru Ioan Cuza University, Iași, Romania

The end of this month will see https://conferences.au.dk/confest2025
CONFEST: August 25-30, 2025 in Aarhus, Denmark.

Microsoft open-sourced (under the MIT license) their VS Code Copilot extension:
https://github.com/microsoft/vscode-copilot-chat

There's a lot of code, and quite expectedly mostly infrastructure code. Still one can learn how they manage searches for the relevant code in the project tree, interaction with Git, analysis of the LLM responses, chats with the user and so on.