Comments URL: https://news.ycombinator.com/item?id=47645039

Points: 2

# Comments: 0

But still disagree: we have cbindgen.

I can't stress out how much important this sentence is. I would even remove the "familiar with rust" part.

Anyone who still thinks it's good to use C/CPP on modern hardware where Rust support is available and good: please print the sentence above and post it all over your place.

Maybe Int

So your program splits into two branches:

1. Nothing branch: you failed to obtain an Int.

There is no integer to use as an index, so you can’t even attempt a safe lookup into something like Vect n a.

2. Just i branch: you do have an Int called i.

But an Int is not automatically a valid index for Vect n a, because vectors are indexed by Fin n (a proof carrying “bounded natural”).

So inside the Just i branch, you refine further:

3. Try to turn the runtime integer i into a value of type Fin n.

There are two typical shapes of this step:

* Checked conversion returning Maybe (Fin n)

If the integer is in range, you get Just (fin : Fin n). Otherwise Nothing.

Checked conversion returning evidence (proof) that it’s in range

For example: produce k : Nat plus a proof like k < n (or LTE (S k) n), and then you can construct Fin n from that evidence.

(But it’s the same basically, you end up with a “Maybe LTE…”

Now if you also have a vector: xs : Vect n a

… the n in Fin n and the n in Vect n a are the same n (that’s what “unifies” means here: the types line up), so you can do: index fin xs : a

And crucially:

there is no branch in which you can call index without having constructed the Fin n first, so out-of-bounds access is unrepresentable (it’s not “checked later”, it’s “cannot be expressed”).

And within _that_ branch of the program, you have a proof of Fin n.

Said differently: you don’t get “compile-time knowledge of i”; you get a compile-time guarantee that whatever value you ended up with satisfies a predicate.

Concretely: you run a runtime check i < n. _ONCE_

If it fails, you’re in a branch where you do not have Fin n.

If it succeeds, you construct fin : Fin n at runtime (it’s a value, you can’t get around that), but its type encodes the invariant “in bounds”/check was done somewhere in this branch.

I was replying to "the US does not get to decide who can have a nuclear weapon and who does not". As much as I agree with that... my previous comment.

We're not talking about a nuclear program.

Instead of letting more countries develop these weapons, we should work on denuclearizing all countries, starting with the US and Russia and their insane arsenals! And maybe build a unified international legal framework for civilian nuclear developments and applications from energy to medical outside of the "security council's" ferule!

A nuclear war cannot be won, thus never fought!

The blog claims that @pool "solves memory lifetimes with scopes" yet it looks like a classic region/arena allocator that frees everything at the end of a lexical block… a technique that’s been around for decades.

Where do affine or linear guarantees come in?

From the examples I don’t see any restrictions on aliasing or on moving data between pools, so how are use‑after‑free bugs prevented once a pointer escapes its region?

And the line about having "solved memory management" for total functions::: bravo indeed…

Could you show a non‑trivial case where @pool eliminates a leak that an ordinary arena allocator wouldn’t?

Could you show a non‑trivial case, say, a multithreaded game loop where entities span multiple frames, or a high‑throughput server that streams chunked responses, where @pool prevents leaks that a plain arena allocator would not?

Sound type systems are equivalent to proof systems.

You can use them to design data structures where their mere eventual existence guarantee the coherence and validity of your program’s state.

The basic example is “Fin n” that carries at compile time the proof that you made the necessary bounds checks at runtime or by construction that you never exceeded some bound.

Some languages allow you to build entire type level state machines! (eg. to represent these transactions and transitions)

Or another (dummy) example transfer(accountA, accountB). Make two types that wrap the same type but one being a TargetAccount and the other SourceAccount.

Use the type system to help you, don’t fight it.

I'm pretty sure Rosenblatt was criticized back then for his non-tangible stupid ideas, and why the hell was his research was funded to begin with.

Decades ago we were calling out these software and now it’s the norm.

Another example along the line: I wanted to extract a frame from a video on iOS, it’s impossible with the built-in tools (screenshot aside) and found that someone built a paid app only for that.

I tell you where we’re heading, we’re screwed.

* build a codegen for Idris2 and a rust RT (a parallel stack "typed" VM)

* a full application in Elm, while asking it to borrow from DT to have it "correct-by-construction", use zippers for some data structures… etc. And it worked!

* Whilst at it, I built Elm but in Idris2, while improving on the rendering part (this is WIP)

* data collators and iterators to handle some ML trainings with pausing features so that I can just Ctrl-C and continue if needed/possible/makes sense.

* etc.

At the end I had to rewrite completely some parts, but I would say 90% of the boring work was correctly done and I only had to focus on the interesting bits.

However it didn’t deliver the kind of thorough prep work a painter would do before painting a house when asked for. It simply did exactly what I asked, meaning, it did the paint and no more.

(Using 4o and o1-preview)