Scala 3 capabilities

[Alan Karp]

https://arxiv.org/pdf/2603.00991

I've only read the abstract so far, but it sounds interesting.

--------------
Alan Karp

[Raoul Duke]

"Types that track capabilities can express a wide range of safety
properties with low overhead."

When static types lead to errors, they can easily be horrendously bad
UX, so i for one would reserve judgment on how much pain using this
would be in practice. (Also, since I am a realist/pessimist, i get the
feeling Scala 3 jumped the usability shark in all sorts of other
ways.)

Copilot AI does say that the Scala 3 features used in the paper are a
rare blend not to be found in other languages, so kudos there.

[Mark S. Miller]

To know what the security properties of an ocap program are, we must reason about it statically. For most ocap practice, we do this intuitively + running tests to try to falsify our intuitions. However, this is of course inherently unreliable wrt hazards one has not noticed. All formal systems for reasoning about the security properties of ocap programs reliably have terrible UX. Type systems in general have been the best way to reduce the UX burden of reliable formal methods. Though type systems themselves can of course have terrible UX. Improving the UX of the type system may or may not be more promising than trying to support the needed formal methods by means other than types.

I'm not sure yet how much of that applies to this paper, but I'm hopeful.

--
You received this message because you are subscribed to the Google Groups "cap-talk" group.
To unsubscribe from this group and stop receiving emails from it, send an email to cap-talk+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CAJ7XQb7NngVymmyku3bxsHVAf-E90zXGeL5UtpPskGUR_PjB6w%40mail.gmail.com.

[Alan Karp]

I've built UXs for capability-based applications using static types, and I don't understand your comment about errors leading to bad UX.  Errors with static types are caught at compile time, so I don't see how they affect the UX.  Building a UX on capabilities is easy with one caveat.  You give each resource an affordance in the UX, which, as Marc Stiegler says, lets you use acts of designation as acts of authorization.  The tricky part for the UX is specifying attenuation, but I don't see how that has anything to do with static types.

--------------
Alan Karp

On Tue, Apr 7, 2026 at 2:07 PM Raoul Duke <rao...@gmail.com> wrote:

[Raoul Duke]

> I don't understand your comment about errors leading to bad UX

You can also read it as DX: the error messages in advanced statically
typed systems can easily be incomprehensible to mere mortals. In
effect, what we really need is a debugger UI for the type checking.
But, even with that, the actual understanding of the logic of the
types can be quite hard. Perhaps AI can help out here - it won't mean
I will magically become fluent, but it might at least be able to
automagically fix things for me.

[Matt Rice]

I'd also add that language-server protocols by providing more
immediate feedback, rather than an
edit, save, compile, test loop. Now when errors happen the point of
the cursor is often in a position relevant
to the error. This has really given both interactive theorem provers,
and static languages a significantly
improved UX.

There is also a question of whether foundational capability types like
sealer/unsealers impose any significant generic/higher order types
which are the typical problem with static type usability. I know i've
done some higher order typed capability patterns which *do* add
significant overhead, such as by using branded sealers/unsealers, and
branded sealed boxes, so you can prove statically that the sealed box
was sealed by the sealer with the same brand which is part of a pair
associated with the unsealer.

That is to say you cannot give someone a "fake"/constant unsealer,
which is like `lambda box => "completely ignores the box so given any
sealed box return this string or something silly"`

Given the relationship between sealer/unsealer pairs and public key
crypto http://cap-lore.com/CapTheory/Dist/PubKey.html
doing that sort of thing you need a type system strong enough to
implement a kind of "perfect" form of public key crypto.
The Emily sealers/unsealers didn't use this kind of higher order
typing, just used normal lambdas and opaque sealed types as boxes.
allowing you to spoof unsealers.

What I'm getting at is that the cost of these guarantees is the more complex UX.

One of the UX issues with static types is that they give an equality
test, but the type system doesn't know which is wrong.
The type of the value does not fit the declaration, but whether the
declaration's type is wrong, or the value is actually the wrong type
isn't
something the compiler itself can tell you. So as the types get more
complex and parametric it increases the burden.

So at least in that sealer/unsealer example, while there is a cost to
using more advanced types,
there is also a tangible benefit in the sense that we can eliminate
some unwanted behavior.
So at least it's not just complexity for complexity's sake.

> To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CAK-_AD5%3Do%3DbPcL1wAB95nUP9DKrDbUSWMtM6hu0KFJ1cX1obEw%40mail.gmail.com.

[Chip Morningstar]

I think the UX that Mark and Raoul are referring is actually the DX (i.e., the “user” in question here is the developer trying to ensure their code is what it’s supposed to be).

Complex type declarations in, say, TypeScript can be a nightmare to both write and read.

Chip

To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z2TYypJEOFTPwURirMnH3ta%3DSvbEOqymR40tPrUdXPSEw%40mail.gmail.com.

[Alan Karp]

Thanks, Chip.  That explains my confusion.  I've seen the same thing in some Rust routines where the type declarations are longer than the actual code.

--------------
Alan Karp

To view this discussion visit https://groups.google.com/d/msgid/cap-talk/6EB2C62A-1848-4F1D-BC2F-357448B66904%40fudco.com.

[Mark S. Miller]

On Tue, Apr 7, 2026 at 5:49 PM Chip Morningstar <ch...@fudco.com> wrote:

I think the UX that Mark and Raoul are referring is actually the DX (i.e., the “user” in question here is the developer trying to ensure their code is what it’s supposed to be).

yes.

 

Complex type declarations in, say, TypeScript can be a nightmare to both write and read.

Yes. Even though TypeScript purposely sacrificed soundness for the sake of a better DX. For formal methods for security, 1) you absolutely do not want to sacrifice soundness. 2) you need fancy type systems that are much harder to understand than TS.

 

To view this discussion visit https://groups.google.com/d/msgid/cap-talk/6EB2C62A-1848-4F1D-BC2F-357448B66904%40fudco.com.

[Mark S. Miller]

On Tue, Apr 7, 2026 at 5:53 PM Alan Karp <alan...@gmail.com> wrote:

Thanks, Chip.  That explains my confusion.  I've seen the same thing in some Rust routines where the type declarations are longer than the actual code.

Rust is indeed a great example. It gives you static confidence of much more interesting properties than classic type systems. In fact, these more interesting properties are so capability-like that other languages, like Pony, refer to them as "reference capabilities", emphasizing both the similarities and differences from ocaps. Pony in particular has both. Neither subsumes the other.

But Rust and other reference cap systems do have a harder DX than classic type systems. Even sound ones ;)

 

To view this discussion visit https://groups.google.com/d/msgid/cap-talk/CANpA1Z3dAyWt8zNqy3HJ3LmMAK0-sg5RN_BVRHQ%3DcRPJ43HzTA%40mail.gmail.com.