AlexTCH

One undisputable advantage of "code copilots", they nudge developers into writing detailed understandable comments.

mistral-small3.1 does not run on Nvidia RTX 3070 even if you're explicitly trying to make it do so. Probably the dated GPU doesn't support some functions.

/set parameter num_gpu 48 in ollama for gemma3:12b supposedly sends all the layers to a GPU, which occupies 7 GiB VRAM and bumps generation rate from about 5 tokens/sec to about 18 tokens/sec.

In the crazy world of Web GIS systems, you download SAT images from a cloud and then remove clouds from the images... 😂

https://dl.acm.org/doi/10.1145/3694848.3694852

Towards Verification of a Denotational Semantics of Inheritance

Peter Mosses mechanizes in Agda (sic!) the proofs from the seminal OOPSLA '89 paper by Jens Palsberg and William Cook on the (fixpoint) semantics of inheritance. That's fucking awesome!!! 🔥

http://pl.ewi.tudelft.nl/seminar/2025/05/07/anuyts/

Extensible types as unknown bialgebras

Andreas Nuyts invents something crazy in the best sense of the word! Unfortunately, he haven't published anything on this topic yet...

Proposing a new intelligence metric to replace the IQ score: LLM-equivalent The size of an LLM that's about as smart as you. Measured in the number of weights, as per usual. Tens of billions, if you're lucky. 😏

Technically, Google search works faster than asking a local LLM, even considering the results page load time. But while you're clicking through "prove you're a human", "consent to our spying cookies" and all that crap between you and whatever Google have found... The local LLM already spit out half the answer...

mistral-small3.1 for ollama weighs in about 15GiB and runs on CPU for some reason...

https://www.kickstarter.com/projects/crowleyaudio/lovecraft-investigations-crowley The folks want to deeply investigate the life and "work" of the infamous Aleister Crowley and present it in the form of a podcast. I still don't know why people call "podcast" any old radio play or other kind of broadcast that they publish on the Internet. I guess that's the term now. Anyways, Crowley had a mind-boggling biography — had the luck of being just the right kind of crazy in the time ripe for that kind of craze — which would be entertaining to learn. Besides, they say the previous "seasons" of The Lovecraft Investigations produced in partnership with the BBC are terrific in all the meanings of the word. I'll check them out too.

deepseek-r1:14b for ollama weighs in about 9.0 GiB (surprisingly) and on inference uses about 6.5 GiB VRAM.

gemma3:12b-it-qat for ollama weighs in about 8.9 GiB (surprisingly) and on inference uses about 3.6 GiB VRAM.

gemma3:12b for ollama weighs in about 8.1 GiB but on inference uses only about 4 GiB VRAM.

Определённо, я уже рассказывал про книжку Рустана нашего Лейно: https://dmkpress.com/catalog/computer/software_development/978-5-93700-199-3/ Но мне не стыдно вспоминать про неё каждый раз. В конце концов, её написал Рустан Лейно — в принципе, этого уже достаточно. 😁

Я уже писал про книжку Камкина? https://dmkpress.com/catalog/computer/software_development/978-5-93700-340-9/ На трёхстах (300) страницах автор обозревает очень широкий круг тем верификации программ: — основы семантики программ и дедуктивной верификации a la Флойд-Хоар-Дейкстра, включая Frama-C и Why3 — теоретически неразрешимая, но практически крайне интересная проблема автоматического синтеза инвариантов циклов, включая использование абстрактной интерпретации — основы SAT/SMT-решателей и алгоритм DPLL — конкурентные программы, LTL и Promela/SPIN — автоматы Бюхи, их связь с LTL и использование для проверки моделей — символьная проверка моделей (за которую дали премию Тьюринга) и NuSMV — плюс использование формальных методов в тестировании программ чтобы читатель всё-таки узнал что-то полезное 😁

Apparently, training neural networks is NP-hard. Training neural networks is NP-hard in fixed dimension Training One-Dimensional Graph Neural Networks is NP-Hard

Also our planet itself constantly produces signs of its existence and evolution. Even if we reset the civilization only one year into the past, we would be very puzzled what happened to Valencia, North Carolina and Myanmar among many other places, and where are all the records and media coverage.

If you look into it, turns out humanity generates signs of its existence with a great speed. The SCP Foundation would face a huge problem covering a reset even 5 years into the past. For example, Starlink engineers would be very puzzled why we already have thousands of satellites in the sky way ahead of the schedule.

https://cacm.acm.org/blogcacm/reversing-the-fossilization-of-computer-science-conferences/ Bertrand Meyer complains about bureaucratization of CS conferences and kinda suggests steps in a better direction (back to substance and innovation). Nothing to do with the FOSS software.