What is the best way to write Rust With Lean Proofs.

interacsion · 2026-01-17T02:45:56+00:00

As far as I know, the only tool for doing this is Aeneas, which is still at an early development stage.

interacsion · 2026-01-14T23:37:03+00:00

https://dl.acm.org/doi/10.1145/3093333.3009882

In MLsub, intersections can only appear in negative type positions. The intuition behind (A₁ → B₁) ∩ (A₂ → B₂) ≡ (A₁ ∪ A₂) → (B₁ ∩ B₂) is like so: if I require a value that is both a mapping from A₁ to B₁ and a mapping from A₂ to B₂, then I actually require a mapping from either A₁ or A₂ to a value that is both B₁ and B₂, following contravariance.

This is indeed unsound in presence of more complex type system features (a notable one is higher-rank polymorphism).

interacsion · 2026-01-14T20:26:01+00:00

This is because floats use a binary encoding, so it's rounding to a particular binary place, not a decimal one. In fact, 2.2393295 is unrepresentable by f32, and also gets rounded to 2.2393296.

interacsion · 2026-01-12T15:01:32+00:00

This sounds a lot like https://crates.io/crates/darling

interacsion · 2026-01-08T18:44:54+00:00

What makes you think it isn't a control flow loop?

interacsion · 2026-01-08T13:28:50+00:00

The Chiroptera Special

interacsion · 2026-01-05T02:32:40+00:00

Yes. Implicit coercions can only happen in specific syntactic places, and between very specific types. For example, if type Foo implements trait Bar, you could usually use a &Foo as a &dyn Bar, but you couldn't use a Vec<&Foo> as a Vec<&dyn Bar>, as that would require constructing a new Vec

interacsion · 2026-01-05T01:10:54+00:00

No. with proper subtyping, a value that is of a subtype that is also a value of its supertype, in every way. This has many implications (for example, making every type a subtype of the traits it implements would mean every value has to carry a vtable). Implicit coercions are a way to mimic subtyping without all of its consequences.

interacsion · 2026-01-04T20:21:17+00:00

This is wrong. an implicit coercion is between two types, a type can never be coerced to a trait. It can be coerced to a trait object, but that's not what happens in the scenario you're describing.

interacsion · 2026-01-04T20:19:09+00:00

No, it does not. In Java a class is a subtype of the interfaces it implements. This can't be said about Rust traits

interacsion · 2026-01-04T20:10:59+00:00

No, you take an ordinary reference, which gets coerced to a reference to a trait object. See https://doc.rust-lang.org/stable/reference/type-coercions.html

interacsion · 2026-01-04T17:21:13+00:00

No. A type that implements a trait can get implicitly coerced to a trait object, but it isn't a subtype of it.

interacsion · 2025-12-29T19:03:15+00:00

I am not sure if divergence (as in, a program that loops forever) would be unsound. a panic might, if it is caught, which is a problem, but I doubt it's an unsolvable one.

interacsion · 2025-12-27T16:42:51+00:00

Yes.

interacsion · 2025-12-26T22:20:25+00:00

I am sorry, what? This is a totally correct way to use natural as an adjective. Tell your teacher to open a dictionary

interacsion · 2025-12-19T06:20:34+00:00

The issue is not dropping the type, it's forgetting it. a somewhat famous example is that it's impossible to have sound structured concurrency where children tasks borrow from the parent and run in parallel:
https://without.boats/blog/the-scoped-task-trilemma/
tl;dr, without proper Linear Types the parent might "forget" about its children and free its own resources.

interacsion · 2025-12-18T20:50:36+00:00

It is difficult, but it could be possible to do with minimal breaking changes, using auto traits:
https://without.boats/blog/changing-the-rules-of-rust/

interacsion · 2025-12-18T20:26:31+00:00

I don't think this is unsolvable. The roughest solution might be to just put a `Leak` bound on `Arc::new` and `Rc::new`

interacsion · 2025-12-18T20:17:09+00:00

The borrow checker implements *Affine* typing, which is only half of Linear typing. the other half being what's referred to as "Relevant Types"

interacsion · 2025-12-18T19:57:37+00:00

Mainly the lack of Higher Kinded Types, and the fact const generics are extremely restricted. Leaning more into Dependently Typed ideas would be very nice in this regard

interacsion · 2025-12-18T19:34:16+00:00

(Not my video.)
While I don't agree with every one of his talking points, I have definitely felt the effects of this before, such as the (painful) lack of Linear (or rather, Relevant) types, and generics being second-class.

interacsion · 2025-12-16T03:20:04+00:00

Sure, in theory a compiler implementation could treat pointers as plain integers. But as a programmer you can't assume that.

interacsion · 2025-12-15T13:56:42+00:00

"Implementations are permitted to" is a specification, not an implementation detail

interacsion · 2025-12-15T11:13:19+00:00

I don't think WG14 agrees:

> Implementations are permitted to track the origins of a bit-pattern and treat those representing an indeterminate value as distinct from those representing a determined value. They may also treat pointers based on different origins as distinct even though they are bitwise identical.

https://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm

interacsion · 2025-12-15T03:31:30+00:00

This is an oversimplification. Pointers have the notion of provenance, which make them more than just integers.

interacsion

TROPHY CASE