In other news. Lawrence Paulson started a series of introductory posts to Isabelle/HOL: https://lawrencecpaulson.github.io/2022/05/04/baby-examples.html

WOW this is mind-blowing: http://liamoc.net/holbert/
A browser-based notebook-style theorem prover for higher-order logics. Aimed at educational applications, and as such can switch between more formal tree-like and a book-style natural deduction proofs presentation.

Here's a notebook about MLTT: http://liamoc.net/holbert/?https://gist.githubusercontent.com/brendanzab/1b4732179b15201bf33fed6dbca02458/raw/mltt.holbert

https://blog.rust-lang.org/2022/05/10/malicious-crate-rustdecimal.html

Rust's Crates.io выходит на уровень NPM и PyPi, так сказать. Печально, но это действительно был всего лишь вопрос времени.

Но моё внимание, как обычно, привлёк следующий пассаж:

When the function was called, it checked whether the GITLAB_CI environment variable was set, and if so it downloaded a binary payload into /tmp/git-updater.bin and executed it.

Это про функцию Decimal::new. Да, она должна просто создавать число.

И кому только может понадобиться разделять чистый код и эффекты в системе типов языка? Зачем? Бесполезная бюрократия на ровном месте!

https://www.youtube.com/watch?v=9MqVfzxAp6A

Alan Kay is at his shit again! That's year-old news actually. Some quotes.

> A great group is smarter than the smartest member. A bad group is stupider than the stupidest member.

> "A committee is the only form of life with 10 bellies and no brain!" — Robert Heinlein
Who said C++?!!

> "... If we succeed in making an Intergalactic Network, then our main problem will be learning to communicate with Aliens ..." — J.C.R. Licklider

"A little company named Adobe" was founded by the guys who invented the PostScript. Insane.

If I ever have enough money to invest in a startup, my first question will be "what have you invented?" Adobe was founded by the guys who invented PostScript, Google was founded by the guys who invented PageRank, what the fuck have you invented?!

https://experimentalhistory.substack.com/p/against-all-applications
"Against all applications".
Not in "Appstore Applications" sense but in "Job Applications" sense.

Writing portable code is hard: https://www.chemistryworld.com/news/structures-in-more-than-150-papers-may-be-wrong-thanks-to-nmr-coding-glitch/4010413.article

The error is the result of a simple file sorting problem. On operating systems without default file name sorting, the script fails to match the files containing a conformer’s free energy with its chemical shift – leading to an overall wrong value.

Which meant the script worked fine on Windows while producing incorrect results on GNU/Linux. This jeopardizes some 150 chemistry papers.

https://experimentalhistory.substack.com/p/ideas-arent-getting-harder-to-find

Good news: worthy new ideas are not harder to find in all areas (art, science, business and what not). Though I suspect ideas might become harder to develop to a "competitive state".

Bad news: doing science indeed becomes harder for all sorts of wrong reasons. 😒

https://livebook.dev/
Jupyter-like notebooks for Elixir but with some twists.

It looks like they aim not at Data Analysis but something akin to DevOps tasks automation. Though they have SQL and visualizations too.

Speaking of which their approach to Widgets (they call them Smart Cells) is curious. Smart Cells are basically a UI to generate some Elixir code which gets then executed in a usual way. At any point you can replace the UI with the code and start rewriting it manually however you please.

Integrated package management through Mix API seems nice and much better than separately installing libraries and importing from different places.

In the end they're building 100% source code backed notebook interface. Well they got me hooked to a degree. 😊

Сохранил себе.
#anime #dataset #visualization

https://arxiv.org/abs/2203.17125
"An Affine Type System with Hindley-Milner Style Type Inference"
Gonglin Li

I think I know some folks who might be interested... 😁

Keith M. Foster breaks down original Oregon Trail while porting it to Python: https://keithmfoster.com/the-oregon-trail/

https://www.youtube.com/watch?v=rkZzg7Vowao
A short interview with Leslie Lamport (of LaTeX fame 😁).

Teaching programming via teaching coding is like teaching writing via teaching typing. Which doesn't make much sense.

and some other great quotes. 😁

https://www.shadertoy.com/view/7dccRr

This is dope! Don't forget to click on the animation. 😉

https://journals.plos.org/plosone/article?id=10.1371/journal.pone.0115069

The choice of an efficient document preparation system is an important decision for any academic researcher. To assist the research community, we report a software usability study in which 40 researchers across different disciplines prepared scholarly texts with either Microsoft Word or LaTeX. The probe texts included simple continuous text, text with tables and subheadings, and complex text with several mathematical equations. We show that LaTeX users were slower than Word users, wrote less text in the same amount of time, and produced more typesetting, orthographical, grammatical, and formatting errors. On most measures, expert LaTeX users performed even worse than novice Word users. LaTeX users, however, more often report enjoying using their respective software. We conclude that even experienced LaTeX users may suffer a loss in productivity when LaTeX is used, relative to other document preparation systems.

O-oh, it's so disheartening! 😢
#latex #msword #study #paper

A reaction to the paper linked in the previous post: https://blog.cr.yp.to/20201206-msword.html

I'd say the reaction mostly points out obvious glaring problems with the original study, but maybe they are not that obvious in the end as long as the paper was peer-reviewed and published?

I'd recommend skipping the first part of the post, everything before the explicit reference to the paper as it discusses simple stuff about list numbering and editing and reference management which MS Word and Word-like systems can do for many years.

Also the post references several other reactions to the study but I didn't follow the links.

Где-то в прошлом году я постил ссылку на https://dcic-world.org/ и отчаянно рекомендовал эту книгу как для самостоятельного изучения, так и в качестве основы для преподавания. И всё ещё рекомендую!

Напомню, что это основательно переосмысленное и переработанное продолжение http://htdp.org/ которая была и во многом остаётся революционной в части методического подхода к преподаванию программирования. Обе книги отличаются исключительной систематичностью: материал подаётся в выверенном порядке, без забегания вперёд или использования неизвестных понятий. Более того, изложение заранее учитывает типичные проблемы студентов и либо явно их предупреждает, либо даёт инструменты самопроверки и самопомощи. В том числе, этот подход поддерживается и специально разработанными языками программирования и IDE, используемыми в этих учебниках.

И тем не менее, Data-Centric Introduction ухитряется пойти ещё дальше, решить ещё больше затруднений, возникающих у студентов, показать больше связей информатики (Computer Science) с "реальной жизнью" (и не только программистов, но и бухгалтеров, маркетологов, учёных всех мастей и т.д.), объяснить ещё больше алгоритмов и дать больше систематических способов построения собственных и ещё больше облегчить переход со специальных языков на общеупотребительные (Python главным образом).

А теперь к инфоповоду для моих повторных излияний. Обе книги в ближайшее время выходят на русском языке в издательстве "ДМК Пресс" и уже доступны для заказа:
https://dmkpress.com/catalog/computer/programming/978-5-93700-137-5/

https://dmkpress.com/catalog/computer/programming/978-5-93700-926-3/

Remember this conference with unpronounceable acronym? Turns put they've released all the recordings quite some time ago. Just click on a talk's title in the schedule.

https://intfiction.org/t/inform-7-v10-1-0-is-now-open-source/55674

Some people were holding their breath for this but I'm not one of them evidently. Inform 7 went open-source almost a month ago. If you don't know what it is, go check it out, it's pretty cool. At the very least pretty unusual.

https://www3.nd.edu/~dthain/compilerbook/
"Introduction to Compilers and Language Design" by Douglas Thain

A free introductory book (PDF is available for direct download) on writing compilers. It spends 3 out of 12 chapters on scanning and parsing which is kinda questionable but at least touches all major topics. As an in introduction should be pretty decent.