Spartan lambda — the Λ for Lacedaemon, the name of the territory of Sparta

Hidden symbolism of System F 😁

https://www.sciencenews.org/article/long-covid-brain-fog-blood-brain-barrier-damage
COVID induced long-term brain fog may be due to brain blood vessels damage. That's not certain, but sounds very plausible at least for a subset of cases.

Устал от городской суеты, от неуёмной молодёжи — хочется на природу, в леса, к вековым деревьям, к ровесникам...

https://www.hillelwayne.com/post/graph-types/

Some time closer to the end of last year Hillel Wayne got puzzled by the question "why no mainstream programming language has neither built-in type for graphs, nor standard library support for them?" He decided to thoroughly investigate the question and interview some people with relevant experiences.

The linked post presents the answers, which are completely unsurprising for anybody who did any semi-serious work with graphs or graph databases. Indeed the four interviewees were unanimous in their issues with the graph libraries and algorithms in general.

Still, it's nice to have all the reasons laid out and discussed in one place, so I suggest taking a look. There's also a link to follow-up comments with curious cases, especially the Rubik's cube. 😊

https://www.youtube.com/watch?v=PPCfDe8TfJQ

A nice talk about applied mathematics and mathematicians, connections to reality, ways of thinking and how far they can take you (I was particularly pleased to find Kolmogorov among other prominent mathematicians mentioned).

https://drive.google.com/file/d/17e_jZ0WwBCeIt0p1ZBF80QAsnIrDpUv6/view
"Математическая составляющая"

Сборник популярных очерков/заметок/этюдов по прикладной математике. Третья часть состоит из более развёрнутых эссе в том числе по более фундаментальным вопросам математики. Возможно, наиболее полезным является аннотированный список литературы для дальнейшего изучения и погружения.

#free #book #pdf

https://github.com/Strumenta/MPSServer

https://strumenta.com/ built an OSS app to run languages (models) built with the JetBrains MPS on a server and expose through an API. This opens up an option of building custom Web UI for the languages/functions instead of running MPS IDE on the client machine.

https://adum.fr/as/ed/voirproposition.pl?matricule_prop=53822&site=adumR#version

A PhD position devoted to formal verification of distributed applications written in Go language in Isabelle/HOL.

Go is so bad they can't write sound distributed systems without formal verification! 🤣

https://www.youtube.com/watch?v=w-IiVeGAydE

WOW! Just WOW!

Apart from the antimemetics stuff (which is surprisingly close to the original), it's a really well-done short movie. The script is tight and to the point, acting is great, very cool lighting, cinematography and color-grading. Unbelievable production value for the money.

Can't wait for the rest! 😃

Пока верующие сидят на жопе, молятся, уповают на Б-га и ничего не делают, нам, атеистам, приходится как проклятым носиться у Него на побегушках!

Old news. Jeremy Howard (of the Fast AI fame) with a cofounder established and "applied AI" RnD lab:
https://www.fast.ai/posts/2023-12-12-launch.html

For now it seems the lab's output only consists of blog posts, but the posts look intriguing, like
You can now train a 70b language model at home

https://www.cl.cam.ac.uk/events/syco/12/
Twelfth Symposium on Compositional Structures
Birmingham, UK, 15-16 April, 2024

They say the talks will be streamed online, but still require registration in advance.

https://sat-smt-ar-school.gitlab.io/www/2024/index.html
SAT, SMT and Automated Reasoning Summer School
June 26 - 29, 2024, Nancy, France

An in-person summer school for PhD and Master students in the field of Automated Reasoning. The list of lecturers includes some big-time contributors of major systems like CVC5, E and Vampire. Highly tempting.

https://www.findaphd.com/phds/project/automated-verification-of-webassembly-programs/?p169824
Fully funded PhD scholarship with Graduate Teaching Assistantship in Automated Verification of WebAssembly Programs at University of Reading, England.

Сидина — те, кто застал CD-диски.

Connecting to the message directly above:
https://www.tomshardware.com/tech-industry/floppy-disk-reliant-san-francisco-train-control-system-spurs-concerns-of-catastrophic-failure-and-it-wont-be-replaced-for-at-least-another-decade

San Francisco train control system was commissioned in the times before computers had hard drives and to this day runs from floppy disks. Now, what do you know about legacy? 😏

Если ты не убираешь говнище из кошачьего лотка, то убираешь лоток из говнища.

https://cogniterra.org/course/38/promo

An official JetBrains MPS course from JetBrains themselves. It says "elementary" but it assumes a basic level of MPS understanding. The course focuses on implementing DSLs together with special editors and code generators for them. Offered for free.

ACM SIGPLAN International Conference on Programming Languages Design and Implementation aka PLDI 2024 is coming:

https://pldi24.sigplan.org/
Mon 24 - Fri 28 June 2024 Copenhagen, Denmark

Early bird tickets and all that...

https://www.cst.cam.ac.uk/conference/structure-meets-power-2024
"Structure Meets Power 2024"

Unfortunately (though very fortunately for a certain minority), it's about Math and Computer Science in particular:

There is a remarkable divide in the field of logic in Computer Science between two distinct strands: one focuses on semantics and compositionality (“Structure”), the other on expressiveness and complexity (“Power”).

The date is 7th July 2024, the event will be held in a hybrid mode, so we all'll be able to look at how well will Power meet Structure. 😁

https://www.youtube.com/watch?v=QGOnUm5HBmo

Another (somewhat dated) talk on how Formal Verification can be fruitfully combined with Property-Based Testing. The authors have a language and a compiler for it that generates the bulk of required definitions and tests. The source is on the Github.