gugagore

I think you're describing "gradual typing", which had lots of promise and attention, but arguably achieves the worst of both worlds: https://www.ncameron.org/blog/a-response-to-a-decade-of-deve...

What it comes down to is a reconciliation between these two views: https://ncatlab.org/nlab/show/intrinsic+and+extrinsic+views+...

I think the "reliability" you mentioned is "type safety". And I think the dynamicism I sometimes miss in a language with static types is, in a bizarre way, the lack of runtime type errors. If you load a configuration file, necessarily at runtime, but the configuration file has the wrong format, an error should occur. What kind of error? In essence, a type error...

Reusing the type checking machinery at runtime is a benefit to some. At the same time, the possibility of type errors (type unsafety) is a threat to the reliability of programs.

I have trouble wrapping my head around it, but I ultimately want the bikeshed with both windows.

Can you comment on the relation been a live programming environment (no separate "staged" compilation. There is always a dev environment, the REPL, in a deployment), and dynamic types?

The typing available in CL, is it like Python type hints in that they don't affect the meaning of a program whatsoever?

Could you provide an example of one of the well written explanations?

Interrupts are a hardware feature on CPUs. You could have software that is effectively checking for events on each tick (clock cycle), and emulates interrupts. But that's what polling is.

I wonder why not embed this in Lean or other theorem prover?

There is often a discussion drawn between a computer algebra system and an interactive theorem prover, but to be honest, I don't fully understand what the distinction means.

I think the quickest way to say it is that there is only one head on a page, and every HTML file needs a head. So if you include one into the other, you either have two heads, or the inner document didn't have a head.

DACs do a zero-order hold, which is equivalent to a pixel as a square.

> But I like to praise it because it represents a hint of what I wish my tooling were like, and would like to see this concept of moldable development spread outside of the Pharo community.

You might like this talk! "Liberating the Smalltalk lurking in C and Unix - Stephen Kell" https://news.ycombinator.com/item?id=33130701

I did spend a day or two on the discord a few years ago, and the conversation was dominated by some conflict over a refector...

What due diligence are you talking about? Personal research? (Genuine curiosity)

I was a bit confused about the key point of patch-based versus snapshot-based, but I got some clarity in this thread: https://news.ycombinator.com/item?id=39453146

Many comments are comparing Glamorous Toolkit to a JuPyteR notebook. It's worth noting that the comparison falls short because Glamorous Toolkit itself, including all of the UI [1], is implemented in the target language.

[1] https://github.com/pharo-graphics/Bloc

I think I know what math is, though I'm not sure. Logical systems of axioms and inference rules?

But I'm even less sure what conceptual reasoning is.

Subtyping is one form of type polymorphism. Others include:

- parametric polymorphism (generics, templates, ...)

- ad hoc polymorphism (type classes are the nicest example)

- https://en.wikipedia.org/wiki/Row_polymorphism I think this one is the most relevant for the record discussion.

I thought it spoke to windows and macOS woes that package management was a third-party concern.

What is the gap between e.g. `apt` and Homebrew?

> While Rust doesn’t fill the same niche as Julia with respect to scientific computing, I really like the safety guarantees around ownership and borrow checker.

From the same discourse thread.

Interoperability across languages with FFI is an option, but it comes at a cost. Even if the two languages have polymorphism, e.g. with parametric types, the interfaces are almost always monomorphic.

> programming is about telling a computer how to actually add 156 with 1571 by adding bit to bit

programming can also be about producing generic solutions that commit to some minimal set of assumptions so that solutions work across a variety of contexts, e.g. regardless of whether your data is floats or ints.

sometimes good engineering is about finding decisions you can avoid making or thinking about. Sometimes you have to decide how to add the numbers bit by bit, but for that particular example, it's even better to not care about how the numbers are added up (which is a detail of the CPU or a bignum library or whatever).

I don't think "type unions" correspond neatly to sums. When I think of a type union in mypy, typescript, Julia, etc, those languages have Union[int, int] as equal to int.

But int + int is isomorphic to bool*int.

The unions you're talking about necessarily require a notion of subtyping, I believe.

Does pip-compile do the same? Or what's the difference?

I was looking for a blogpost from many years back about features Windows cannot provide, because it would result in logical inconsistencies if multiple applications used the feature. The blogpost gave examples like setting the desktop background or file-application associations "definitively" from applications, and mentioned at least one example of two applications fighting resulting in some chattering in the Windows UI.

I thought it was Raymond Chen's blog but I haven't been able to find it. I thought someone here might recall and have a pointer.

fixed link: https://goosetaco.notion.site/Drinking-SICP-hatorade-and-why...

If you have any light to shed, I'm wondering about inductive data types and their expressive necessity here: https://news.ycombinator.com/item?id=42166709

I recently came across the notion that you need inductive data types (and can't just use Church encodings) if you want to do theorem proving, like proving that `0 != 1`.

I threw up some content up here: https://intellec7.notion.site/Drinking-SICP-hatorade-and-why... , along with an unrelated criticism of SICP.

I'd like to better understand what the limitations are of "everything is just a function".

The problem you describe with waiting for tests for unrelated code changes (or potentially related but you want to skip it for the reasons you describe) is a problem that seems to deserve a solution even within a single monorepo.

What are the solutions? You would need multiple merge queues.

Surely the git SHA is "a form of versioning", isn't it? Yet I don't see how that form of versioning helps.

What robot is performing what surgery unassisted?

Generally (not just for LLMs) this is called student-teacher training and/or knowledge distillation.

Lego education used to be called "Lego Dacta". https://www.brothers-brick.com/2020/01/31/a-history-of-lego-...

The question then emerges: how do we program these things?

Sara Acour has some answers, e.g. https://scholar.google.com/citations?view_op=view_citation&h...

I thought that rust's compiler was indeed written to be incremental first. Check a sibling comment of mine for reasons why I thought so.

Other comments have addresses many always of your comment. The constantly changing part is also an important feature for recompilation being more efficient than recompiling from scratch each time. You can read about it here: https://rustc-dev-guide.rust-lang.org/queries/query-evaluati...

There is recording of a talk on YouTube from Niko Matsakis that goes into the motivation.

In conclusion, you don't really want to optimize for the batch use case, even outside of IDE support.