nylonstrung

Everything touching this ecosystem (Gas Town, Dolt, Beads) seems like the absolute nadir of vibecoded slop

This specific community has been a Schelling point for some of the worst engineering practices I've ever seen and a desire to abstract away all details of code to LLM personas like the "Refinery" and "Deacon"

The 18th century called, they want their Malthusianism back

> What will happen in the oft-ignored developing world?

Did you even read the prompt

This is cool, I have been working on something similar with Lean4 albiet focused on compiling to Substrait

This is pretty well done as well https://github.com/palladin/lean-linq

This looks great, I'll be excited to see this progressively become pure Zig and drop C++

Would be great to have something like Kontakt without all the cruft

The next 12 months will see OAI and Anthropic spiral into into increasingly hyperbolic PR stunts, manufactured benchmarks and underhanded attempts at regulatory captures

I'm sure they have nothing to rival this on a price/performance basis and have already given up on that

Greg Egan's 1994 Permutation City actually depicts Malaysia using cloud compute to model cyclones and mitigate them with weather manipulation

Very prescient

What do you think makes it a bad foundation to build on?

It would be stranger to me that Kimi switched to GLM's tokenizer than that GLM added multimodal like Kimi and Deepseek both did recently

This project is cringe and I really hope we see less stuff like this

I'm almost confident the architecture is the result from some kind of pivot from blockchain gaming.

Previously they talked about "testnet" and you use "energy credits" to pay for services. They also described aspects as being similar to smart contracts.

Naming the game "Bitcraft" circa 2021 is a big tell as well

It's actively unhelpful even for the most "non-technical" of users to further anthropomorphize LLMs and "agentic" workflows that boil down to moving plaintext around

The design is cute but this is an abstraction that simply has no reason to exist, and is the opposite of what better UX looks

I have no idea how spinning up a MicroVM solves the problems this paper talks about and I doubt you actually have programmed GPU kernels ever

Well mojo handles it by introducing an additional step of lowering code to MLIR as an intermediate representation. Something that can be done with C++ as well

I don't disagree but I don't think this one is a reason we should ever restrict or condemn a technology

> it is a mirror, and augmentation and reveals really inhuman takes and thought processes from people who are on the longer lever in society

When someone uses their keyboard to search for CSAM or write hate speech we can't blame the keyboard instead of the individual

Gemini was a bad choice of example but how would open-weights model one can self-host on their local device be different than the electric motor in your line of thinking

This doesn't sound like someone who is uninterested in understanding software though, everything they said talks about how they like being able to learn from it. They didn't say anything about making slop or replacing the need for knowledge

Yeah most normies I know who dislike it just generally are not interested in it or think it is dumb and are annoyed by hearing about it so much

And the people who actively hate it almost always relate it to a broader pre-existing worldview about the downfall of society, the climate being destroyed, financial markets being a ponzi, oligarchy having too much power etc

Classifying dense matrix multiplication and autoregression as a munition is equally as dumb as when PGP was classified as one

Clearly there are people who enjoy the slop though, otherwise it would simply get no engagement and then get hidden by the algo like 99.99% of YT videos

I do think this is true but I think it also reflects negatively on the general populace that this new technology is evaluated in terms of the negative effects on their consumption pattens

Transformer models solved the Protein Folding problem in totality but they are categorically "bad" because more of the videos in my feed are low-quality or the advertisement for a cheeseburger looks fake

It's predictable but I do think the entire technology is being collectively processed through the lens of media consumption which is sort of tip of the iceberg of what it does and honestly the least important dimension of it

I think a lot of what's underlying this is just a big difference in general societal optimism/pessimism

In polls 80-90% of Chinese say their country/govt is headed in a positive direction vs <30% in US

Order of magnitude? It's 10x more expensive now?

For columnar databases, I love Vortex' Dtypes which lets you attach semantic context in a logical type to what is essentially compressed Arrow https://docs.vortex.dev/concepts/dtypes#logical-types

Yeah I really dislike that you need neovim or VS to benefit from Infoview

Haven't tried it but there's this community-made REPL https://github.com/leanprover-community/repl

Amit Patel's website is so good, some of the best explanations of concepts like pathfinding, perlin noise etc

https://www.redblobgames.com/

> Does Lean have a type for "list containing only prime powers"?

You can wrap a base type with a proof which is called bundling

inductive PrimePower where | mk (n : Nat) (prf : IsPrimePower n)

So in this case the type checker will not allow construction unless the proof demonstrates they are prime powers

The prf part gets erased at runtime so there's no overhead. You could also use a constraint/refinement type like you talked about and it's more flexible as it relates to using list operations like map filter reverse etc.

This is not remotely true, it was designed as a general purpose functional programming language and the adoption by mathematicians only came later with the creation of Mathlib.

It's not a DSL but has very powerful metaprogramming capabilities that make it great for creating DSLs

There's nothing the core language lacks compared to say Haskell

I don't think issues like syntax and schema compliance are the level of problems where verification comes into play

In this case it's more that the underlying declarative systems function as they should across any possible states or configurations

You mentioned policy and the policy language Cedar uses Lean formal verification in this way, not to verify that the specific policies users create are sound but to ensure that the declarative policy engine itself cannot produce any invalid or unwanted configurations

I think the gap is real and for it to be resolved, the spec language needs to be elevated to a source of truth and possibly do some degree of codegen, which is currently not well realized with Lean

The analogy I'd make is to the idea of "type driven development" that buf/protoc represent, where one defines their types and schema in proto and then types for specific languages are generated from that

The limitations there however is that proto is not a programming language and inflexible/inexpressive whereas Lean is one of the most expressive languages to date