Ericson2314

See, that people are shocked by this is the problem. The whole field of AI has proceeded as alchemy, not science.

Some of this is because "the Bitter Lesson" type experience, but some of this is because of the idea that "we're making machines to do things we don't know how to do" bakes in inscrutability into the very definition of the field.

I was excited about the "Neural Networks Are Already Clean" piece not because alignment, which I don't think much about as a non-EA, but simply because we can do better engineering with whiteboxes than blackboxes. Now, here we are, doing it.

> [code below]

    let dyn_array = fn (erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }

Yes, but array(len, t) has a dynamic layout. Your system needs to understand that that is OK because `pointer(array(len, t))` still has a static layout. You need to understand that pointee-monomorphization is not necessary. You can do special hacks for the `pointer` type constructor, but then you cannot eta-expand it (i.e. wrap in a one field struct). To make this work in a first-class way, so custom data types can have type parameters that do not need to be monomorphized, you need your type system to be layout-aware.

Also, you can do

    let dyn_array = fn (dynamic erased t : type) -> record { len : int @@ dynamic, data : pointer(array(len, t)) }

There is no need to force the element type to be static. The array itself doesn't care. The pointee is already dynamic-layout either way.

> [code below]

    let vtable = fn (erased t : type) -> record { print : pointer(t) -> string, ... }

    let dyn_print = record { t : type @@ dynamic erased, vtable : pointer(vtable(t)), data : pointer(t) }

The problem with this is that `vtable` is being called with a dynamic-erased argument, but it itself requires a static type. That means the whole thing is dynamic (well, depending on exactly how the modalities work). But do want to statically know it is a record with a print field, etc.

> static layout would require parameterizing on the layout of t, so I see your point

:) See https://docs.rs/stack_dst/latest/stack_dst/ for example, which tries to hack it in Rust. It would be much nicely to do it safely!

I happen to agree that extreme inequality is bad for Capitalism, but I still think it is a moot point here.

The overall world carbon gini coefficient is less than the wealth coefficient. And this is totally expected: ultra-rich people cannot consume fast enough to pollute more in proportion to how much richer they are. For example, to do this would private jets, they would have to be paying for other people to ride separate private jets, as there is only so much time they want to spend in an airplane themselves.

A carbon tax might not hit private jets hard enough, but it would definitely hit "regular people's" (still rich by global standard's) air travel, and that would lower a lot of emissions.

Yet another person confusing "allowed" vs "required"

PBT testing and fuzzing are basically the same thing in my mind.

What's funny though is that the reasoning needed to say some sampling is comprehensive....makes it closer fo proofs! AFL — coverage-based fuzzing — was the original innovator here, but imagine an interpreter — code coverage in the interpreter itself isn't so good, you also want to explore the interpreted program!

This is why "is my testing comprehensive?" is actually an open-ended problem that, in the limit, is just as hard as formal verification.

I suspect we're basically going to see a convergence here. Randomized testing can be called "Monte Carlo formal verification" hehe.

I don't think you want to avoid this complexity:

- OOP is existential types where the layouts share some sort of shared prefix (e.g. pointer to vtable, fields in common, etc.). To accurately model such things (and they occur in FFI), you need to separate types from layout, and hold the "supertype's layout" fixed.

- A classic use-case of dependent types is dynamically-sized arrays, and "tensors". When you have a pair (L: Nat, V: Pointer(Array(N, T))), you have a layout behind the pointer that is dynamic, but you don't want to conflate this with arbitrary types of the pointee.

Failure to deal with this in fully generality will force you to go down Rust's path of ad-hoc arrays and "dyn trait", which is actually more complexity.

> Not entirely, since Syl uses static data to describe types' runtime layout. Allowing dynamic there would require overhead (e.g. a uniform representation).

This is where it is crucial to distinguish types from layouts. "uniform representation" means the layout is static while the type is dynamic. But this isn't an overhead in the sense of dynamic checks or lack of erasure.

Having static (erased) layout parameter and dynamic (erased) type parameter is the fully-general solution: monomorphization per layout, not type. And the caller decided whether to thread a layout parameter, or fix a single layout.

Yeah I think this project could use a little guidance.

The real magic with types parameters is that they can both be dynamic and erased!

> That is, Syl is dependently typed at compile time and simply typed at runtime.

This is not full dependent types. And there is no reason to limit oneself this way for performance, because again dynamic + erased has no overhead.

- More public transit (I am personally working on it)

- Cheep Chinese EVs

- Another attempt (ugh) at getting Detroit to cooperate

- Denser housing

- Higher gas/carbon taxes

should all contribute to people driving with gas less in the relatively near future.

Training, producing open weights, can be done by the government.

Inference can be a commoditized business.

If the farmer didn't buy electric tractors, it's not really your fault. But if you drive a gas vehicle yes it's your fault.

There is no right answer re blaming the customer or owner. This is push vs pull.

I'm talking about white collar workers working remote on a multi-day HSR trip all the way from the Continental US, through BC-CA, AK-US, RU, etc.

Yes, this is a very, very, very large Capital project :)

But we're talking 100,000s of different parts that can be soddered on a board. That's not one factory.

If we were serious about domestic Manufacturing we'd both be doing massive automation and open borders with Latin America. You need the massive inflow of temporarily cheaper labor.

Automation picks up up as immigrants run out.

Actually with Carbon inequality, the problem is that driving and flying is not expensive enough!

If they take both supply chains of consumption and ownership into account, they are straight-up double-counting, unless they are separating opex and capex or something.

This is mostly a distraction because so much Carbon pollution is within supply chains, and therefore not wise to ascribe to individual consumers.

The exceptions are driving and flying. 8M is more than the private jet users, I assume. Getting rid of ICE driving is going very well (outside fossil-Luddite America).

Getting rid of flying is harder, but I fully support a rail bridge across the Bearing Strait. I'll take long sleeper trains working remote before I get to my old world vacation proper. This is good for circadian rhythm too.

The real question is, do current training methods allow one to learn this when training on enough, say, assembly, or can the weights only be achieved via hard-coding?

A fun and important thought experiment about the the space of nerual networks vs the image of current training methods.

Most discourse conflates neural networks and trainable neural networks.

What's lazy then?

I took lazy to mean "waiting for the gov rather than doing it ourselves". I'm saying that may be true for the initial catch-up but it's not true for the work going forward.

Did you read the linked piece?

The data is "there" in some some sense, but it is messy, coarse-grained, and arrives slowly.

Once the office is familiar with Git, we can start the conversation about having the new version of the US code instantly ready when a bill is passed. In particular, rather than voting on the informal patch, congress should vote on the final result. (bills are patches, but votes should be on the new state with the patch applied.) Then the office merely supervises the Git repo, and is freed up to focus on other codification tasks, such as hyperlinking definitions, overseeing formalization of the tax code like France did, etc.

Previous discussions often foolishly conflate version control with "no force pushing of any branch" and "all branches must be public". That is stupid. Vote trading will continue to make drafting happen in secret, since it is simple game theory that an "atomic transaction" of many possibly-unrelated things is an efficacious coordination mechanism. This is just about getting the final version and its already-public history cleaned up and mechanized to the greatest degree possible.

It's easy and fun for volunteers to put in the effort once. It's doing the work on an ongoing basis that is less fun and less motivating. The ongoing work --- done without modern tools --- is already that office's responsibility, so this should be too.

I am saying that Martin-Löf would see his work in Lean, not mathlib. Mathlib is a library. In Lean you can "contain" classic reasoning to certain parts of the code base, and that is also true in the original MLTT: you can postulate classical axioms as functions in scope.

Because I have want my government to use the right tool for the job.

I don't want to privatize this core civic function to some NGO.

No Type Theory won: Per Martin-Löf is still alive and should be able to confirm his work lives in some form in Lean. Zermelo and Fraenkel would be utterly confused, however.

What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).

I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.

If they are serious on this, they will work on lab robotics and fancier and fancier organoids for automatic testing.

(No one please propose automated mice testing or the EAs will have an aneurysm, haha.)

Between 55 feet and 55 meters, how poetic.

The Hacker News Community (hah) needs to lobby hard to pass a law (what boostrapping!) to require the https://en.wikipedia.org/wiki/Office_of_the_Law_Revision_Cou... to maintain the repo as part of their duties, and do it retroactively for the entire history of the US Code.

It's a simple idea; it's cheap; there are no outstanding technical questions; it benefits almost everyone. Let's get this done.

Don't worry about that. Even if we only saw voted-upon revisions in the Git history, it will still be a huge improvement.

Version control for the public parts will make both public and secretive law-drafting better.

Yeah it's crazy how many people are in denial of this.

Storage has been making impressive strides, but the cliff here (in storage and transmission, the latter of which we in the US still are sucking at) puts nuclear back in the running.