cben

There is also Snap! (https://snap.berkeley.edu/) which starts very much like Scratch but has higher ceiling. The deepest pedagogical benefit is you can easily build for him custom blocks — even custom control structures — to give the scaffolding that will let him focus on the programming style/aspects you want him to learn at that point.

Reminds me of this android gqme: https://play.google.com/store/apps/details?id=ru.DmitryLomak...

I'll add The Unix Programming Environment, by Kernighan and Pike. Like K&R, the examples it picks "happen" to teach so much more than you came to learn :), e.g. anatomy of version control, some language design, basics of interpreters & compilers.

I seriously nominate Lauren Ipsum by Carlos Bueno as a _better_ Alice story. It's exlipictly about CS, but is also chock full of math, philosophy and some life advice. It's almost a GEB for kids.

The author of Oil Shell has some of the best writing on why unix shells are an important niche to push forward.

Unix (and later the internet), by enforcing "narrow waists" [1] like a flat stream of octets for all communication, is inherently polyglot. You can have richer data types inside programming languages, and indeed Python, JS, Rust etc. all have vibrant ecosystems of packages with rich internal APIs. But at some point you want to interface software written in widely different languages, and Unix encourages a particular style of command-line interface which is "dumber" — array of arguments, flat file(s) I/O — but is easy to compose across languages.

Therefore, whatever you do in "better" languages, there remains a need for a glue layer whose main job is not doing computation itself but invoking external processes. There is tons of arguing about the threshold — whether a particular task is better expressed inside a "rich" language or by plumbing together commands — but it doesn't change the need for a good shell language to exist.

Now, is bash a great shell language? NO. It's a pragmatic choice for historic reasons. One day we'll do much better. [2]

[1] https://www.oilshell.org/blog/2022/03/backlog-arch.html [2] https://github.com/oilshell/oil/wiki/Alternative-Shells

#!/usr/bin/env python3

Mere `python` will remain ambiguous for years whether you'll get 2 or 3, but explicit `python3` doesn't have that problem.

A list I built once of such options for commands: https://github.com/fish-shell/fish-shell/issues/3164#issueco... You are right, very little consistency :-(

In some cases you really need the \0 delimiters for safety, but a large portion of safe scripting in shells is merely about handling arrays of strings, without joining nor splitting them on whitespace. bash does have arrays and "${array[@]}" syntax but it's pretty horrible (and needs the `shellcheck` linter to keep right). Some more modern shells e.g. `fish` do much better on this.

Sorry, i misspoke about "Church numerals". The book uses them to represent non-negative integers by lambdas but here that wasn't necessary, TypeScript allowed a simpler representation of N as a the type of an N-deep nested list.

What's common to both approaches to building arithmetic is starting from zero + a "successor" function T. That approach is called "Peano arithmetic".

I still recommend that post/video (and the book in general) but I have to admit there is no 1:1 correspondence to the TypeScript going on here.

Still, it'll teach you some general maneuvers for bootstrapping computation out of almost nothing , qnd once you're comfortable with those, you can read things like this TypeScript post, or aphyr's original Haskell post, which bootstrap computation out of sjighly different" almost nothings" and without following the details still have a high-level idea of where it's going (like the poor interviewer in the story ;-)

There are 2 components here. One is the "type metaprogramming" - (mis)use of the type system to implement to do compile-time computation, mainly by using parametrized types as kinda-functions + type inference for kinda-pattern-matching.

The other is building up basic "data types" by pretty standard lambda calculus > LISP route. "Understanding Computation" book has a great chapter 6 on that, which is available in blog & video forms on https://computationbook.com/extras - Here, Church numerals were used to represent numbers. - booleans & conditionals here didn't resort to the lambda representation you'll see in the book, but relied on type conditionals builtin to TypeScript. - The names "Cons" & "nil" are a ringer for LISP-like building of lists, and recursive processing of lists, from a "pair" data type.

https://3fx.ch/typing-is-hard.html is a neat summary, and yes the situation is worse than most programmers would guess: Most industry languages, including "boring" reliable ones like C++, Java or Rust have _undecidable_ type systems;( and quite a few are unsound as well.)

This doesn't mean type systems are useless! But as GP said there are tradeoffs, and suspiciously many language designers gave up "clean" properties like guaranteed-terminating compiler, or you know actually guaranteeing run-time safety...

BTW, TypeScript documents where it's unsound and why consciously made those choices: https://www.typescriptlang.org/docs/handbook/type-compatibil...

Wikipedia has nice summary of "Atomic battery" designs that are not simply RTGs: https://en.m.wikipedia.org/wiki/Atomic_battery#Non-thermal_c...

Due to price, when you buy motors/sensors/hubs, you'd want them to be compatible with future buys. LEGO used to have several systems but now pretty much converged to one "Powered Up" interface: https://brickarchitect.com/powered-up/.

The app is indeed neat & powerful. Performance is limited by official firmware being "dumb", it reports sensor values and takes commands, all computations actually run in the app. However, what's cool is an essentially unbrickable bluetooth bootloader letting you try alternative FOSS firmware — see https://pybricks.com/.

also https://echa.itch.io/pocket-robots-test-chamber

"Understanding Computation: From Simple Machines to Impossible Programs". I knew many of topics and enjoyed it nonetheless. Highlights:

+ Very insightful chapter on different flavours of language semantics, and specs vs implementation.

+ The standard CS automata/ grammars stuff, but with working code.

+ Fun chapter on FizzBuzz in lambda calculus (it's also the free sample+video). Whats vool there is not just showing you _can_ compute everything (of vourse you can) but that you can build high-level constructs so the resulting code is todally clear.

+ A bit of the standard CS computability stuff, but then gets into esoterically minimalistic yet turning-complete stuff like 1D cellular automata.

+ Type checking as a form of partial evaluation, and some other "symbolic" stuff you can do with partially-evaluting interpreter. Some overlap with dependent types - but a more pragmatic less type-theoretic angle.

Author uses a carefully selected subset of ruby, introduced in a short intro - big props for being thoughtful about that.

P.S. +1 to Mazes book too (which is not as conscious about its ruby use, fun anyway)

A much smaller in scope but pretty fun introductory game: https://echa.itch.io/pocket-robots-test-chamber

Funny — I've been recently re-leafing through it to find _just_ the Babylonian infodumps. (though I failed at "skip ahead 5–10 pages whenever there is an action scene", because they're too good :-)

For me the blurring of religion/biology/code boundaries was brilliantly interesting (even if factually unconvincing). If you skip these infodumps, consider going back later.

-> for those who like that meta-liguistic angle, Laundry Files series by Charles Stross may be fun. It has some similar "Enochian" language used for programming zombies / magic / etc. (the tone is quite different though, more of a horror comedy, and varies between books as he's parodying different material.)

-> on the "collapse of government" angle, Diamond Age by Stephenson is almost a direct continuation. plus very cool nano-tech. (2nd half has few scenes using humans bodies in a gross way.)

-> if you like a large Quest crossing both physical and intellectual world, well, almost any Stephenson book :)

See https://github.com/fish-shell/fish-shell/issues/3164#issueco... for incomplete but large survey of NUL flags.

Takeaways: (1) There is no consistency in flag names, even --long ones (2) impressively many tools do support it! Note that some affect only input or only output. (3) All do NUL-terminated, not NUL-separated. That's fortunate — matches \n usage, and gives distinct representations for [] vs [""].

The point of oil that there are really basic things like safe quoting that shells should do well, yet none of the posix shell do!

Functional: there are interesting shells like Elvish. But it really goes PowerShell by adding internal rich data pipelines that dont have a unixy stream-of-bytes representation. Oil does NOT go that way; it works on stuff like QSN to make pure unix interconnects more robust.

On a type to be named _separately_.

To-be-named-at-runtime is simply dynamic typing. It's polymorphism without static typing.

Generics based on type erasure, e.g. Java, wrap that with a type system hoping* to prove safety at compile time, yet compile to a single dynamicly typed implementation, that does not use this type info at runtime.

Generics based on code generation / specialization, e.g. C++, generate distinct run-time implementations with the type hard-coded. (Though you can plug in dynamic typing by making the hard-coded type a pointer.) In C++ this is more than optimization, it's semantics — you can specify distinct behavior for specific types.

JIT compilers can start from a single dynamic-dispatch implementation and generate specialized implemetations for some types, bridging the divide.

But in any case, the common meaning of "generics" is not merely polymorphism, it's polymorphism plus a type system where you _name_ the type you're gonna use.

* https://3fx.ch/typing-is-hard.html#java

A) monitors do report physical size to the OS!

https://en.wikipedia.org/wiki/Extended_Display_Identificatio... > 21 Horizontal screen size, in centimetres (range 1–255). If vertical screen size is 0, landscape aspect ratio (range 1.00–3.54), datavalue = (AR×100) − 99 (example: 16:9, 79; 4:3, 34.) > 22 Vertical screen size, in centimetres. If horizontal screen size is 0, portrait aspect ratio (range 0.28–0.99), datavalue = (100/AR) − 99 (example: 9:16, 79; 3:4, 34.) If either byte is 0, screen size and aspect ratio are undefined (e.g. projector)

This is not perfect of course, may be defeated by cheap adapters, KVM switches, splitters that send image to 2 monitors, etc... And projectors can't know the projected size. More importantly, people sit far from a projector screen; absolute size is not very meaningful without knowing how far away people sit!

You're right that a window spanning multiple monitors has mixed physical size, but that's an edge case that doesn't invalidate taking physical size into account as a goal. Some OSes do re-scale UI when a window fully moves into a monitor with different scaling.

It makes a big difference when a language spec (such as Scheme) requires it. If only some implementations have it, and you can't assume it when coding, then it's "just an optimization". https://en.wikipedia.org/wiki/Tail_call#By_language has a list.

Yes and no. Learning UNIX is a bit like learning LISP - the parentheses don't look "exteremely pleasant" but having (1) a shared serialization format (2) common programmatic interface (3) a culture of REPLs makes everything much more discoverable and gives you power you would never get where each interface is a shiny bespoke thing.

There a lot of kludges, especially around teletypes/terminals, yes. But the common interchange format being ~ASCII~ UTF-8 makes learning the ins and outs way more pleasant than if everything gets connected by COM, .dll APIs, inscrutable .inf files or whatever Microsoft thinks up at a given decade (you can notice I've stayed away for a while)...

Now Excel stands aside as as environment where learning _was_ pleasant, everything had an inspectable representation and a shared interface! Despite arrays bounds and reuse-by-copy-paste being messy, spreadsheets remain a sweet spot of bringing power to "low-code" users. I didn't look into this specific project enough to say where falls on lock-in-vs-interoperability scale, but IMHO the world needs more "spreadsheet plus" experimentation so I wish them the best...

https://blog.burntsushi.net/ripgrep/ explains in detail _how_ it's so fast, and is a great reading on practical performance engineering.

The interface is nearly 1:1 with `ag` (and the older `ack`). One notable difference is that ag enables `--smart-case` by default, so it treats an all-lowercase pattern as case-insensitive, while `rg` doesn't, you need an explicit `rg -i`. (or set it in a config file, but I'd rather not learn defaults that won't work out-of-the-box on other machines).

I agree with everything you say, except I have a lower bar of "meaningful".

> one possibility is simply that “dynamic type checking” is meaningless.

If I take your quotation out of context, this was the assumption of some people who separated languages into simply "strongly" vs "weakly" typed, by which they meant "checked by compiler" vs "not checked". It's incorrect though, and is the reason for separate "static" vs "dynamic" distinction.

C is a famous example of static (checked at compile time) but weak (≈ unsound) typing — compiler will happily accept programs that corrupt memory in all kinds of ways. mutating "const" variable, freeing used memory, crashing, remote code execution, and more... I don't think there are any invariants that a C compiler can enforce.

Scheme, Python, Lua, Javascript etc. OTOH, have no static (= compile-time) type checking, yet they maintain some invariants! An object that has pointers to it will not be freed; An object's type is known, and will not change (well, some class transmutation is allowed but some not, an int will not turn into an array); Some types are immutable; You can never divide a string / string! etc...

Moreover, by maintaining run-time metadata about object's types, they can tell you specifically that an operation raised a TypeError. Thus these languages are strongly typed at run time.

IOW, I'm arguing that anything that blows up at run time is checked IFF it tells you it was a type error. This is meaningful compared to C segfaults that tell you nothing :-)

---

The Java paper https://dl.acm.org/doi/pdf/10.1145/2983990.2984004 shows an interesting subtlety. "Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM" — yet they present unsound programs that "type-checks according to the Java Language Specification and is compiled by javac, version 1.8.0_25".

What gives? If a bad program compiles, how come JVM is still sound? See, Java has two type systems!

- JVM is the runtime, intended to be capable of loading even untrusted bytecode yet still maintain some type invariants. It manages memory and type metadata, and for this bad program will correctly identify type violation at run-time: "When executed, a ClassCastExceptionis thrown inside the main method with the message “java.lang.Integer cannot be cast to java.lang.String”"

- The compilers uses a distinct more complex static type system. The question of soundness is: can any program that passed the compiler cause JVM run-time type errors?

  + Java language allows you to write type casts.  These are deliberate "trust me" holes in the *static* type system, whose specified semantics is: JVM will check type at run time and raise exception if not as programmer promised.
    As https://typing-is-hard.ch/#what-about-unsafe-casts says, since these are deliberate, and fall back to meaningful run-time type checking(!), let's ignore them — redefine "soundness" as: can a program with no exclicit casts cause a run-time type error?

  + Generics only exist in static type system!
    They are invisible to JVM (aka "type erasure"), they compile into dynamically checked casts.  
    Their soundness goal was that the compiler can prove these implicit casts will never fail — e.g. you can only put candies into ArrayList<Candy>, so arr.get(0).eat() is guaranteed to give you a candy you can eat.
    That paper demonstrates a simple 17-line program with no explicit casts that compiles yet causes run time type error.

---

If you think what type soundness means, ALL statically typed languages have 2 type systems! There are execution semantics — what it means to, say, compute number + number. And there is a static language of talking about types that aims to predict / prove the types that will be involved at run time. Static checking fails if they don't match. Dynamic checking largely fails when you don't do it :-) But also when you erased info you needed to do it.

When we were forced to start use Jira a year ago it was kinda maybe acceptable, but every week someone in the organization adds a new custom field to issues, so it's growing scarier than bugzilla...

Behind the scenes, stashes _are_ branches! It's just UI on top of them, optimized for specific use case. You don't have to use it if you don't like it.

Now staging (aka index) is special behind the scenes, making the model more complex for Al users.

We at $CONTENT_FARM fell in love with this envsubst-as-a-service paradigm, and built our own with A/B testing. We then discovered we can apply it not only to our content but also to our bash codebase!

Now looking for funding to add evolutionary algorithms, combined with the best ideas from TRAC and m4, to make this a joy to maintain.

the "black" frixion pen we use on elfinbook is a bit grey, not full black, but no problem seeing at all - like a regular pencil. a blue one actually looks even better, seems to have thinner strokes.

We only did 1 clearing cycle so far, and paper is back to practically white. but microwave was not enough, wet cloth worked better.

The paper is somewhat glossy.

TeXmacs is also completely distinct from TeX! It does use TeX-inspired layout algorithms, with modifications to make them better fit real-time typesetting as you type. It's also striving to be an environment for interaction with other tools, (not unlike Jupyter Notebook).

If you want a structured scientific web editor with collaboration, check out also https://www.fiduswriter.org/. Built on top of ProseMirror.

But Fidus is closer to "WYSIWYM" like LyX — structured editing with "acceptable" typesetting, and TeX export for high-quality typesetting. TeXmacs shoots for true "what you get" high-quality typesetting as you edit. Mind you, the edited model is structured in "what you mean" spirit (with quite good UX to "see" the structure), not flat "slap formatting on characters" model typical of WYSIWYG editors.

Well, with `gzip --rsyncable` and similar (most compression tools have such a mode), it's technically possible to compress first then dedup! To be precise it's "chunk first, then compress", which still admits a 2nd "chunk, then dedup" pass to reuse data, but not as efficiently as a combined "chunk+dedup+compress each chunk"...

`gzip --rsyncable` and friends are mostly useful for when you already have compressed files on your filesystem, and want to sync/backup them byte-for-byte. Of course the benefit is lost unless most compressed files in the world are produced with such mode, and sadly most aren't :-(

The author of `zsync` did various experiments confirming gzip --rsyncable then sync is sub-optimal, and implemented a somewhat crazy "look inside" approach that can sync compressed files byte-for-byte AND very efficiently:

> gzip --rsync does fairly well, with both rsync and zsync transferring about 410kB at the optimum point. zsync with the look-inside method does much better than either of these, with as little as 140K transferred. > -- http://zsync.moria.org.uk/paper/ch03s03.html

IIUC though it's more of a "2-files sync" scenario like rsync, not applicable to "chunk everything then dedup" approach of borg and similar tools.