"Сначала в моей жизни всё шло через жопу, а потом случился запор."

https://spritelyproject.org/

A whole family of (research) projects in secure distributed federated computing and data exchange. In particular,

Goblins implements CapTP, the Capability Transport Protocol, which has such features as distributed acyclic garbage collection ...

Lots of super interesting links from that page.

— У нас безмозглый шторм.
— Может, мозговой штурм?
— Нет.

https://ciechanow.ski/gps/

Very thorough interactive explorable explanation of how GPS works from the very basics to relativistic effects on clocks. With interactive 3D visualizations! 😃

The Pinch-Hitter Syndrome: People whose job it is to do just one thing are not always so good at that one thing.

From https://statmodeling.stat.columbia.edu/2009/05/24/handy_statistic/ That's a real gold mine of wisdom!

"Analysis of a connection between dish washing and self-reported well-being indicators in adolescenten and adult females" PhD.

Information Security is hard.

GitHub learned from an internal discovery by a GitHub employee, that GitHub Pages sites published from private repositories on GitHub were being sent to urlscan.io for metadata analysis as part of an automated process. This internal process was implemented before the private GitHub Pages feature was released and provides metadata that is used during human review of potentially malicious or abusive GitHub Pages sites.

To view the name of the private repository on urlscan.io, you would need to have been looking at the front page of urlscan.io within approximately 30 seconds of the analysis being performed or have specifically searched using a query that would return the analysis in the search results.

-- А как это он коронавирусом заразился?! У него ж и сертификат о вакцинации есть!
-- Да просто вирусы малограмотные пошли, сертификатов не читают...

https://github.com/SciML/SciMLBook

A solid course on combining Machine Learning and Differential Equations (pretty recent field of study dubbed "Scientific ML") using Julia language. It at least mentions many deep and important topics like numerical stability, sensitivity analysis, profiling and optimization. Not even mentioning pretty elaborate explanations on bigger topics like Automatic Differentiation.

My guess it's best for quick intro to the field for people who already have a formal education in diff equations and ML methods. Familiarity with Julia is a bonus. 😊

https://towardsdatascience.com/is-the-normal-curve-too-good-to-be-true-c7cf2fd33997

A post about rare applicability of normality assumption and robust hypothesis testing methods (that don't assume normal distribution).
The post itself does a poor job explaining the problem, the methods to circumvent it and their properties. But it does contain links to actual explanations (Wilcox's book in particular) and libraries implementing these methods.

Finally watching https://www.youtube.com/watch?v=RItz1VPMQTI
It's a real pleasure to watch, a masterclass on presentation and full of insights.

"Going from 'testing is good for you, you should do it' to cases where you have no other way but do it." That's powerful.

https://arxiv.org/pdf/1810.07951.pdf
Don't Unroll Adjoint: Differentiating SSA-form Programs
Michael J Innes, 2019

https://proceedings.neurips.cc/paper/2020/file/9332c513ef44b682e9347822c2e457ac-Paper.pdf
Instead of Rewriting Foreign Code for Machine Learning, Automatically Synthesize Fast Gradients
William S. Moses and Valentin Churavy, NeurIPS 2020

Две статьи, посвящённые (обратному aka reverse-mode) автоматическому (или алгоритмическому) дифференцированию функций, представленных в форме Single Static Assignment aka SSA.

Статьи во многом являются взаимо-дополняющими. Первая рассматривает дифференцирование более высокоуровневого SSA представления до компиляторных оптимизаций, а вторая — более низкоуровневого после (большого количества) оптимизаций. Как следствие, первая статья даёт общее введение в обратное дифференцирование и рассматривает его расширение на низкоуровневые конструкции, такие как условные переходы, фи-узлы, чтение и запись в ячейки памяти. В это время вторая статья уделяет основное внимание ещё более низкоуровневым аспектам: теневой памяти (shadow memory), кешам, обработке указателей, в том числе — вызовам функций по указателю.

В любом случае, обе работы полагаются на "классические компиляторные техники", такие как dataflow analysis, alias analysis, abstract interpretation, и оптимизации. И потому представляют собой интереснейшее расширение "поля деятельности компиляторщиков" в сравнительно новую, но стремительно набирающую популярность, область.

https://www.youtube.com/watch?v=kEf_MTqeXWg
Ethics in Research and Development

A surprisingly practical talk and practical approach to ethics with references to actual tools (checklists at least).
(Bonus content: a question from Dana Scott himself.)

John Harrison of HOL Light fame works for Amazon proving elliptic curve cryptography...

http://www.stochasticlifestyle.com/when-does-the-mean-and-variance-define-an-sde/

Looks like an open research question still. If someone needs a nice MSc thesis topic or something. 😉

https://www.hillelwayne.com/tags/crossover-project/

Хорошие новости для всех, кто (как и я) именует себя "Software Engineer". Да, мы на самом деле можем считаться инженерами!

Более того, накладывать заплатки на заплатки и подпирать костылями -- это старые добрые инженерные традиции. Можно сказать, скрепы.

Но мы можем и лучше. Имеет смысл стараться.

Freek Wiedijk himself shared this gem! 😃

https://behemoth.cl.cam.ac.uk/search/

Natural language based search through Isabelle libraries and AFP for theorems, definitions and alike.

https://arxiv.org/abs/1905.05970
HolPy: Interactive Theorem Proving in Python
Bohua Zhan

The code: https://github.com/bzhan/holpy

Yep, they indeed implemented Higher-Order Logic in Python. And a Web interface in Vue. Sounds very hip but actually the interface is pretty nice, suggestions for proof steps are very good. And in general it's very fun to mouse-click your proofs! 😃

В Inria порываются создать пиринговую сеть сертифицированных машинных доказательств: https://www.inria.fr/en/towards-internet-proof
Звучит, конечно, классно, но что-то мне сомнительно, что это будет пользоваться популярностью в обозримом будущем...