ux266478

11 ms·

121.
by ux266478 3mo ago
Sure, but what I'm saying is that still doesn't make it nice to use as a proof assistant. As you say, the UX isn't there, no matter how much more terse the type system is at certain things in native semantics. Idris is design
122.
by ux266478 3mo ago
In the context of the conversation, it doesn't actually refute the point though, which is that explosive danger is contingent on a much broader set of relations than simple energy density. Gasoline just demonstrates the disconnect. Tac
123.
by ux266478 3mo ago
I mentioned in another comment, but that worse user experience is also going to exist with Idris. It's not a theorem prover, you can just use it as one.
124.
by ux266478 3mo ago
That's not quite right, Haskell's type system is fully turing complete. Strictly speaking, it can encode anything any other program can. If we put aside language extensions, I can see a pragmatic and ergonomic limitations obviousl
125.
by ux266478 3mo ago
> lean4 doesn't let them formalize results outside of zfc. A small correction: Lean 4's native semantics are DTT, not ZFC. Formalizing results for TT is arguably easier, it's the default. But you can use it for any foundat
126.
by ux266478 3mo ago
What semantics do you use for your HOL library? I scanned around but documentation on that page is a bit sparse. The github repo goes to a random user's page, and all I could find there was this unrelated repo: https://githu
127.
by ux266478 3mo ago
> Metamath is based on set theory, and would therefore address some concerns one might have with the propositions-as-types philosophy used by Lean Isn't the entire point mathematicians adopted Lean where they spurned Haskell is beca
128.
by ux266478 3mo ago
I have so much gratitude to the frontier companies who did all the extremely complicated research and development, model by model. It already feels difficult to remember how much capital it really took. Thank you for getting us to this poin
129.
by ux266478 3mo ago
He didn't say that, and I didn't say that, because in fact neither of us were talking about just settings, so that's a pretty curious idea to be addressing. > No combination of settings is going to make them outperform Ant
130.
by ux266478 3mo ago
And I think you didn't understand what I wrote, so let me reiterate: Of course policies are equally ineffective at strictly governing the behavior of local models. Why would that change? The actual problem is that somebody is attemptin
131.
by ux266478 3mo ago
The ultimate difference isn't necessarily down to remote vs local. You can run a "local" model on the cloud the same way you could on a local machine and have all the same control over it. You can modify the weights, inject b
132.
by ux266478 3mo ago
Which is true as a tautology, but not in the way you mean. The problem isn't the hijacking of classifiers, that's incoherent. You bypass a stochastic classifier to hijack the reasoning model, and potentially bypass the stochas
133.
by ux266478 3mo ago
As parent implies, they're testing the wrong control mechanism. Why are you using policies instead of real controls over the weights and inference pipeline? Well the answer is that VC-backed companies decided AI is not a domain expert
134.
by ux266478 3mo ago
A good setup will cost you the same as a decent house in a major metropolitan area. And then the price of a used car to upgrade your electrical to handle that kind of load, and get the cooling setup you need.
135.
by ux266478 3mo ago
> Not after the pathways are tokenized and enter the model. There's no internal separation. There's no internal separation. It's not possible, either. That's not accurate in the slightest. Steering vectors, SAEs, circ
136.
by ux266478 3mo ago
In the case of Prolog, term and goal expansion are arbitrary compile-time execution mechanisms, completely isomorphic with macros, and are referred to as macro mechanisms. The characterization of it not being "compile-time macro execut
137.
by ux266478 3mo ago
A binary has a startup time of like 20 milliseconds, the overwhelming majority of that is setting up page tables iirc. While that's a lot for a small cli utility called in a loop, it's really nothing for a desktop application. I
138.
by ux266478 3mo ago
The problem is that the type of developer you're talking about is the kind who invents a thousand excuses about anything. It doesn't begin and end with different languages. Using a different subset of their favorite language? A di
139.
Cross-Platform CLI and GUI Tools with Tcl/Tk(cgicoffee.com)
5 points by ux266478 3mo ago|1 comments
140.
by ux266478 3mo ago
The distinction does make sense, as castles (formally speaking) are medieval structures, but clearly that didn't matter because the map has other ancient acropoleis. Even putting that aside, the relationship between 'aκρόπολη&#x
141.
by ux266478 3mo ago
It's definitely older than that. Originally, way back in the mechanical days when super-computing was hyphenated, it was about how many millions of instructions per second could be handled. That changed in the 1960s with a series of CD
142.
by ux266478 3mo ago
> the dominant workload for a supercomputer was thought to be physics simulations - and they often benefit from high numerical precision. It still is. Just like how "mainframe" used to be a very general word, and over time gain
143.
by ux266478 3mo ago
> then they could’ve also put a stop-gap on investment volume to protect the economy against over-reliance? Which instantly collapses the load bearing bull market. They can't do that for the same reason they can't do anything a
144.
by ux266478 3mo ago
Well, that's them doing the same thing, yeah? They can't say that they want voter picture IDs for the real reason (partisan electoral strategy), so they have to constantly litigate electoral fraud and the whole parade.
145.
by ux266478 3mo ago
> But thats also an admittance that the American labs can’t compete on merit anymore Merit was never competitive. Mass consumption habits select hard for cost, and this is an industry driven entirely by scaling factors. If you can scale
146.
by ux266478 3mo ago
Which is to say they didn't have much of an idea at all, because it really didn't exist in much the same way. In fact, this is still a inaccurate characterization for exactly that reason. On the basis of copyright, take for instan
147.
by ux266478 3mo ago
> DIY hobbyists may also find it more difficult or impossible to source parts for their projects. I mean not really. A quadrocopter is a remarkably simple thing made out of extremely generic parts: 4 DC motors (and ESCs), a radio, a comp
148.
by ux266478 3mo ago
The things you listed are very far downstream of the start of American industry, which is in primary resource extraction and processing. Which is you know, what actually built the country. The media industry has always been materially irrel
149.
by ux266478 3mo ago
Never let possibility get in the way of a value-signaling business decision, I always say.
150.
by ux266478 3mo ago
> Our society is pretty aligned that distribution is another kind of harm. As well as possession. I don't actually know if those are different for CSAM, but I would assume so because they are for drugs.

More ›