Vale VS verona

Not to be confused with Vale[0].

[0] https://vale.dev/

The article says they created a deterministic hypervisor that runs all pseudorandom behavior from a starting seed to enable perfect re-playability.

But that's all we know so far. I'm assuming there'll be some sort of fuzz testing, and static analysis or some defining actions that your software can perform.

Honestly it sounds a lot like it has a lot of crossover with what the Vale language is trying to solve: https://vale.dev/, but focused on trying to get existing software to that state instead of creating a new language to make new software already be at that state by default.

Why go through all the trouble when you can do this: https://www.hylo-lang.org/ and not spend a second thinking of lifetimes? No, copies will not be issued unless necessary.

Or why not keep exploring this idea as well? More research-oriented than the first one right now, though, so take it with a grain of salt: https://vale.dev/

Another relevant language might be Vale (https://vale.dev), which is aiming for "perfect replayability": https://verdagon.dev/blog/perfect-replayability-prototyped

Interesting. Very low level though and C(++) centric. She there any thoughts on combining the hardware and OS features with rust or https://vale.dev ?

Use a runtime memory management solution that's cheaper than garbage collection (see Vale)

This seems like a tool I'll be using, and this is an almost meaningless criticism, but why the name?

There's already the Vale programming language (https://vale.dev/), but moreover, I don't get the meaning of "vale". You could call it something like Englint which actually hints its purpose.

According to this FAQ, snmalloc was designed for the Verona language:

https://microsoft.github.io/verona/faq.html

Unfortunately, I cannot find any significant code samples for Verona on the website or in the GitHub repo. There are a few types defined in a pretty low-level way:

https://github.com/microsoft/verona/tree/master/std/builtin

I think the future lies in figuring out how to get the benefits of that secret sauce, while mitigating or avoiding the downsides.

Like Boats said, the borrow checker works really well with data, but not so well with resources. I'd also add that it works well with data transformation, but struggles with abstraction, both the good and bad kind. It works well with tree-shaped data, but struggles with programs where the data has more intra-relationships.

So if we can design some paradigms that can harness Rust's borrow checker's benefits without its drawbacks, that could be pretty stellar. Some promising directions off the top of my head:

* Vale-style "region borrowing" [0] layered on top of a more flexible mutably-aliasing model, either involving single-threaded RC (like in Nim) generational references (like in Vale).

* Forty2 [1] or Verona [2] isolation, which let us choose between arenas and GC for isolated subgraphs. Combining that with some annotations could be a real home run. I think Cone [3] was going in this direction for a while.

* Val's simplified borrowing (mutable value semantics) combined with some form of mutable aliasing (this might sound familiar).

[0] https://verdagon.dev/blog/zero-cost-borrowing-regions-part-1... (am author)

[1] http://forty2.is/

[2] https://github.com/microsoft/verona

[3] https://cone.jondgoodwin.com/

Their approach lines up pretty well with how we do regions in Vale. [0]

Specifically, we consider the "spine" of a linked list to be in a separate "region" than the elements. This lets us freeze the spine, while keeping the elements mutable.

This mechanism is particularly promising because it likely means one can iterate over a collection with zero run-time overhead, without the normal restrictions of a more traditional Rust/Cyclone-like borrow checker. We'll know for sure when we finish part 3 (one-way isolation [1]); part 1 landed in the experimental branch only a few weeks ago.

The main difference between Vale and the paper's approach is that Vale doesn't assume that all elements are self-isolated fields, Vale allows references between elements and even references to the outside world. However, this does mean that Vale sometimes needs "region annotations", whereas the paper's system doesn't need any annotations at all, and that's a real strength of their method.

Other languages are experimenting with regions too, such as Forty2 [2] and Verona [3] though they're leaning more towards a garbage-collection-based approach.

Pretty exciting time for languages!

[0] https://verdagon.dev/blog/zero-cost-borrowing-regions-overvi...

[1] https://verdagon.dev/blog/zero-cost-borrowing-regions-part-3...

[2] http://forty2.is/

[3] https://github.com/microsoft/verona

Does this count? https://microsoft.github.io/verona/

What about new Rust that "Microsoft Research" trying to "explore" https://github.com/microsoft/verona/blob/master/docs/explore.md ?

Fun fact: the person who created Pony, Sylvan Clebsch, has been working on a Microsoft Research project called Verona. From it's README [0]:

> Project Verona is a research programming language to explore the concept of concurrent ownership. We are providing a new concurrency model that seamlessly integrates ownership.

https://github.com/microsoft/verona/tree/master