Dependent types are part of it, yeah! There are definitely some things I dislike about Rust which I am not planning on including, mainly lifetimes and some ways they handle pointer mutability. One thing I particularly dislike about Rust is:
let x = vec![1,2,3];
let a = &mut x[0];
let b = &mut x[1];
swap(a, b);
This is not allowed. And actually in the compiler’s mind it’s for the same reason as this:
let x = vec![1,2];
let a = &mut x[0];
x.push(3);
a = a + 1;
Which is definitely not safe and should be rejected. But the compiler cannot reason that the above case is actually safe, because they both fail to compile for lifetime reasons.
Another thing I’m working on are “patterns” which are like enums on steroids. In Rust you cannot define how an enum is laid out, thus requiring optimizations for types like Option<&T> to be in the compiler. In evergreen this will be in the language via a similar process to trait implementation.
The compiler statically tracks “where” everything lives. It also knows “when” the “where” is valid.
Each “where” is called a plane, which is a tree. The stack plane contains all your function calls memory, a structure allocated on the stack has a child plane for each field. The compiler tags which plane something is from at compile time and tracks when it dies.
Things do get complicated in scenarios like:
fn max(a: &usize, b: &usize) -> &usize {
if *a > *b { a } else { b }
}
In such a scenario the compiler tags the result with both of the input planes. However, you cannot define add a postcondition ensures clause to make it more precise
Sounds a lot like group borrowing from Valen, but that one still has annotations like `entity in world.entities[] mut`. Are you tracking the same things implicitly with post conditions?
Allocations live in their own plane, the root allocated typed being the root node of that plane. For threads, I’m still working on that, don’t have a super cool answer yet
Another thing - when a value is moved or dropped the plane’s type changes from T to shape(T). shape(T) contains unspecified data but has the size and alignment of a T. So you couldn’t safely prove that a moved out/dropped shape(T) is a T
This only works if you make every allocation its own plane, and scope all borrows to the lifetime of the plane, with a move terminating all borrows, at which point this is equivalent to rust, just with confusing jargon.
Correct, every allocation is its own plane. The nice thing about this model is that you don't need to explicitly call out lifetimes. I also believe that lifetimes aren't really a good model of what actually happens in memory. This model is more powerful because it understands relationships between planes in memory, which Rust's model doesn't. This is why it requires mutable borrows to be unique which is oftentimes overly restrictive. For instance this is not valid Rust:
let x = vec![1, 2, 3];
let a = &mut x[0];
let b = &mut x[1];
swap(a, b);
Because Rust doesn't really know the difference between the whole Vec an element within the vec. Therefore it treats any mutation as one that could potentially invalidate anything with the same lifetime and doesn't compile. So I believe the plane model to be strictly better because it allows for this and still prevents the real scary thing:
let x = vec![1, 2];
let a = &mut x[0];
x.push(3);
a = a + 1;
I’m not quite sure I understand your question. But if x is a vector of things that contain allocations, the compiler will track a plane for them and represent them sparsely as needed be.
The compiler tracks all of the currently living planes. The compiler tracks from which plane each borrow is borrowed. Once the plane it is borrowed from dies that borrow is no longer valid
Since you are replying, I’ll go ahead and you answer…
In a sibling comment I said the types seem more likely to be refinement (or Liquid) types instead of being full-spectrum dependent types. Is this correct? I certainly haven’t been through enough of the docs to be confident, but I took a swing when I posted my comment.
What I’ve showcased is definitely not full fledged dependent types. Support is planned via ideal generics but it’s lower on the priority list to nail down
The introductory examples look more like refinement type (or Liquid types) which are limited to those operations and restrictions one’s that are provable by the compiler utilizing a restricted subset of operations and computational constructs subject to deterministic proving via SAT solving. I’m going to look closer at the docs so I could be mistaken on that point. It certainly seems to have taken the ownership and ‘borrowing’ concepts for memory semantics from Rust at a quick glance at the first few pages.
Dependent types can be achieved via “ideal Generics”. Very undocumented and not ready to commit to how they work yet, but the basic idea is that a type can be generic on a value.
Yeah it definitely looks like refinement vs actual dependent types. I do the same thing here[1] in my language (pardon the mess). Adding liquid types to basically rust is IMHO a good idea.
Completely coincidentally, we're just about to launch a service that does exactly this (API access to uncensored open models)! We have a waitlist at the moment but will be live very soon!
There is very little information that is illegal by itself. At least in the Western World, and especially in the US. The question is how far you get into the territory of aiding and abetting a crime
But the reasonable defense is that the intended use cases are legal. The home page list a couple, and the 'writing fiction'/'helping authors' case alone covers almost everything. An author asking you how to best conduct a terrorist attack or how Meth is made are perfectly normal. Maybe even tame, compared to what some authors tend to research
More seriously though, I think we should be fine: we don't host any content, and what people do with the models is their own responsibility (legally speaking, in our jurisdiction, at least according to Claude -- we're talking to a real lawyer next week). Like any other provider, we offer no guarantees of sane, safe, or accurate results.
Thanks for bringing up a service like this, it's quite important. A few serious questions if you don't mind.
Confidentiality? Do you use any sort of logging and if not do you have a way to guarantee that your hosting providers are not snooping?
Price vs Vast or Runpod? If i have a very large or a very small workload do you have a competitive rate vs a gpu provider that offers private gpu access?
Subscription vs Api costs? Do you only offer api rate or will you offer discounted tokens for subscription? Subscription friendly towards open source harnesses such as omp?
Heretic ablation vs other methods? KL divergence scores? Do you post train the weights yourselves or do you offer weights trained by other organizations and is this information available on the service?
Cache hit/miss pricing policy? 90/10 or a different cache pricing policy, and how long do conversions stay in kv cache?
Quantized cache and model? Do you offer a choice if i want a quantized model for speed or a quantized cache? If not do you publish the information?
SGlang vs vllm or other inference engine? Do you publish your engine stack details?
Thank you kindly I find the competition in this space very lacking.
These are great questions, thanks! I'll answer them in turn, in a list because I like lists.
* Confidentiality: no logging, third party analytics, or anything like that. More details in our Privacy Poilicy [1]. Our hosting providers will have their own policies, but we're not running a super private service like Proton or similar. Might do some kind of secure tenancy in the future if there's demand.
* Price: I think Runpod vs per-token are very different beasts and for different purposes. I really can't make a direct comparison, as it'll be based on use case, but we're going for convenience over price, so all else being equal I'd expect us to be more expensive for most users anyway (edit: i meant "than other API providers"! We'd definitely need to be cheaper or at least competitive with spinning up your own cloud infra. We'd have parallelism and economies of scale on our side for this). We have a lot of experience with running and optimising open models though, so that's part of the value proposition too.
* Subscriptions: Only API for now. Maybe subscription later but honestly we prefer simplicity. My own experience with subscription plans is that they're usually sold at a huge loss at first, then the price creeps up as the service is enshittified. That feels like a bit of a scam to get users, and that's not really what we're about. We want to provide something specific, and aren't really concerned about scaling as fast as possible. Maybe we'll provide subscriptions if there's a real demand for it, but no plans at the moment to do so.
* Methodology: we use abliterated models, but I've been advised to hold off talking about that for now. Might make a blog post about this though (when we have a blog).
* Cache: yeah about 90/10 for pricing. We're still trying to find the sweet spot for tuning eviction. Running LRU with no guarantee/storage at the moment, could probably be less aggressive with retention, but that also has privacy surface area implications. Ongoing conversation.
* Quantisation: my brother in christ, everyone runs quantised. :) We're initially targetting FP8 on most models, but have had great results with MXFP4 though. If we can pack more concurrency onto nodes without losing quality, we'll reflect that in pricing. Or we'll offer as a separate model for cheaper and give users the choice. Edit: I see you were asking specifically about speed, which MXFP4 doesn't improve, but maybe if there's demand we'll run other qaunts for speed increase, especially on the larger models.
* Engine: vLLM gang all the way! For now at least, as it's what we have most experience with, and we find it the most flexible. We've been experimenting with SGLang though, and there's definitely some interesting optimisations we could do with it.
Hope this answers your questions, at least the ones I could! The irony of that hasn't escaped me!
Improper use is that of the user, not inherent to the tool.
Scolio: guns. Respondeo: guns are much more specialized (one-use) than knives. Proper use of sharp knives when what was shipped was a butter knife is understandable.
(The simile is not fully overlapping but should give the idea. The instrument must be flexible; if it is misused it is then a responsibility of the abuser.)
Generating blackmail is not illegal, using it to blackmail someone is. Generating libel is not illegal, publishing it publicly is not illegal either although you can be sued over it.
Generating worms and computer viruses is not illegal last I checked, but disseminating them is.
My point is that generating is not illegal but sending is. Your whole point hinges on legality, so the distinction between legal and illegal seems pretty key.
Its amazing how biased that source is and how much it buried the lede. They were arrested for participating in a riot where someone attempted to murder a police officer. That's not just someone criticizing ICE on social media. If it was, half the posters in any political thread on HN would already be arrested.
Would love to get a sub. Ive currently got three separate subscriptions to the models above and would be great to combine them.
Coincidentally, I'm Read teaming and checking security issues for a company with the same name as you.
This reminds me of an article [1] (that I think I may have even seen initially on HN) analysing what writing looks like when treated like TV (consciously or subconsciously). It's a fascinating read and it made me more mindful of interiority in my own writing.
That AI consumes it at an abnormally high rate, presumably.
The claim never made sense to me either, I can only assume those that regurgitated such claims never worked with HPC or even general datacenters before.
Was recently talking to a (non-technical) friend about this, she was surprised after talking about the "insane water use for AI datacenters" when I responded that open-loop cooling is pretty rare for a datacenter and I've never actually seen it used before, versus closed-loop (or just regular air-based cooling) which has no real noticable water consumption.
Problem with data centers is that companies want to build them near densely populated areas that already have problems with water supply and high utility bills.
1. They don't HAVE to use water. Air cooling, closed loop cooling, waste-water cooling, and so on, are options. Easy to regulate. Evaporative cooling is more energy efficient though, but a complete non-issue in places with abundant water and a non-option elsewhere.
2. Datacenters have been shown to reduce utility prices. They provide suppliers with previsible long term demand which allows for cost-effective network and production planning.
That AI data centers are drinking up local ground water for cooling. It isn't (or wasn't) nonsense, though. It was/is a real thing, though it seems to be on the out in favor of closed loop cooling after the massive and still on-going public outcry.
reply