Настолько старый и нишевый, что успел подержать первый печатный сборник пирожков. : 🏆
🤡3👍1💯1
https://lawrencecpaulson.github.io/2022/10/12/verifying-distributed-systems-isabelle.html
A guest post by Martin Kleppmann on Lawrence Paulson's blog. Martin explains the basics of distributed algorithms verification in Isabelle/HOL. As the main tools he employs (heavily parametrized) functions, maps (which are secretly functions too), inductive predicates and inductive proofs with a slightly custom induction principle (and variable generalization).
A guest post by Martin Kleppmann on Lawrence Paulson's blog. Martin explains the basics of distributed algorithms verification in Isabelle/HOL. As the main tools he employs (heavily parametrized) functions, maps (which are secretly functions too), inductive predicates and inductive proofs with a slightly custom induction principle (and variable generalization).
👍3
If for some weird reason you decided to write something a layperson can understand there's a tool to help you: https://splasho.com/upgoer6/
On the other hand you can reverse it and try to come up with the most obscure words no one knew were out there! 😂
On the other hand you can reverse it and try to come up with the most obscure words no one knew were out there! 😂
🎉1
Software Requirements Specification to specification is what meta-irony to irony.
🤡2
https://sillycross.github.io/2022/06/11/2022-06-11/
Not all Intel performance cores are created equal! On the flip side all the efficiency cores seem to be indeed created equal. Hmmm... 🤔
Not all Intel performance cores are created equal! On the flip side all the efficiency cores seem to be indeed created equal. Hmmm... 🤔
sillycross.github.io
Bizarre Performance Characteristics of Alder Lake CPU
TL;DR: Some of the P-cores in Alder Lake CPU can exhibit highly unstable performance behavior, resulting in large noise for any benchmark running on it. UPDATE: A colleague of mine reported that the b
👍1
Чтобы научиться ездить на велосипеде нужны дополнительные колёсики. Такие, которые внутрь принимают.
🤡2
ФИДО снова набирает популярность: https://fidoalliance.org/what-is-fido/ ! 😂
Но я разочарован, что они предлагают использовать биометрию вместо пароля. Rookie mistake.
Но я разочарован, что они предлагают использовать биометрию вместо пароля. Rookie mistake.
FIDO Alliance
FIDO Alliance is focused on providing open and free authentication standards to help reduce the world’s reliance on passwords, using UAF, U2F and FIDO2.
Йа — конкретный дед: то забываю выпить таблетки, то забываю, зачем вообще их пью...
🤡3
Со мною вот что происходит
Ко мне мой старый друг не ходит
А ходят в праздной суете
Разнообразные коте...
Ко мне мой старый друг не ходит
А ходят в праздной суете
Разнообразные коте...
😢1🥱1
Вспоминаются нетленные строки
"Кто-то жрёт таблетки, а кто-то колется"
По молодости мы думали, что это про наркоманов, но оказалось, что это просто про людей среднего возраста и диабетиков...
"Кто-то жрёт таблетки, а кто-то колется"
По молодости мы думали, что это про наркоманов, но оказалось, что это просто про людей среднего возраста и диабетиков...
👍5😢4🤡1
https://p-org.github.io/P/
Another "AWS secret weapon" (after TLA+) and again a formal specification language for distributed systems. State machines based. With contributions from Microsoft Research.
Another "AWS secret weapon" (after TLA+) and again a formal specification language for distributed systems. State machines based. With contributions from Microsoft Research.
p-org.github.io
P: Modular and Safe Programming of Distributed Systems
"Задача человека — каждый день выдавливать из себя жлоба".
Тогда задача жлоба — каждый день выдавливать из себя человека? 🤔
Тогда задача жлоба — каждый день выдавливать из себя человека? 🤔
🤡1
https://www.inference.vc/implicit-bayesian-inference-in-sequence-models/
Another approach to understand what the heck Large Language Models are actually doing. From "everything that works works because it's (secretly) Bayesian" perspective. 😁 Still deep technical dive with several useful side-references inside.
Another approach to understand what the heck Large Language Models are actually doing. From "everything that works works because it's (secretly) Bayesian" perspective. 😁 Still deep technical dive with several useful side-references inside.
inFERENCe
Implicit Bayesian Inference in Language Models
This intriguing paper kept me thinking long enough to decide it's time to resurrect my blogging. It aims to explain the surprising abilities of language models to perform in-context learning, i.e. to solve learning tasks embedded inside prompts.