isubasinghe's comments

On: Creusot helps you prove your Rust code is correct

[isubasinghe]

Creusot works on functionalisation if I recall correctly. It translates to coma (https://coma.paulpatault.fr/language/program.html).

Verus encodes directly to SMT.

Creusot may gain some more automation perhaps from this approach.

On: Verus is a tool for verifying the correctness of code written in Rust

[isubasinghe]

Oh hey I worked on this :)

On: F-35 is built for the wrong war

[isubasinghe]

Hmm, this: https://en.wikipedia.org/wiki/List_of_aviation_shootdowns_an...

indicates what the author said is true.

The majority of these losses are on the ground.

On: Ryanair may increase commission to staff identifying oversized cabin bags

[isubasinghe]

Makes perfect sense, if the excess fuel costs outweigh the commission costs

[krisoft → isubasinghe]

It has nothing to do with the fuel cost. This is what ryanair's website says about oversized luggage: "Passengers who bring an oversize bag (over 55x40x20cm) to the boarding gate will either have their bag refused or, where available, placed in the hold of the aircraft for a fee of £/€ 70.00 - £/€ 75.00."

Ryanair earns every time they identify an oversized bag at the boarding gate. They just share some of that money with their staff.

[seanhunter → isubasinghe]

How does size of an item in the cabin correspond with excess fuel? In particular, how do large items cause excess fuel if they are in the cabin, but not the hold?

Remember that the mass of something is the same if it is in the hold or in the cabin, and just because something is large doesn't mean it necessarily has a large mass.

[poszlem → isubasinghe]

Yeah, of all the shady things Ryanair does, this one actually makes sense from a fairness perspective.

[sct202 → poszlem]

Only if the staff is fair. Frontier in America pays their staff $10 per bag identified and when they first started, some gate agents went wild trying to get that $10. There were videos of bags that cleanly fit in the sizer but passengers were being charged and threatened with being blocked from the flight if they didn't pay quickly.

[thaumasiotes → isubasinghe]

No, that would only be true if the commissions were the only cost of the program.

[sokoloff → isubasinghe]

The €75 baggage fee outweighs the commission cost.

On: The SeL4 Microkernel: An Introduction [pdf]

[isubasinghe]

I believe only certain versions and on certain architectures is seL4 verified for. There are no bugs found at the C source code level for these builds of seL4.

[ryao → isubasinghe]

This issue appears to have affected all architectures. This issue was present in the specification against which seL4 was verified. You can say that there are no bugs by virtue of it following the specification, but if the specification was wrong and in this case it was, then were there really no bugs?

[isubasinghe → ryao]

There is always a specification, the question is "was this issue found against a version of seL4 that had been fully specified or not?".

I worked at the lab, I wasn't aware of any bug/issue on the fully specified kernel, that is why I am unsure if this counts or not.

I would need to have a look at the source code and proofs to confirm.

[ryao → isubasinghe]

How does “This issue was present in the specification against which seL4 was verified” not imply yes to that question?

[vacuity → isubasinghe]

Even if it's not exactly seL4, there's good value in taking inspiration for design elements. It would still be a lot more robust than commodity operating systems.

On: Ask HN: What runs L4-related microkernels/hypervisors these days?

[isubasinghe]

Was at UNSW recently, can confirm that apple doing special L4 stuff right now.

On: Piracy Is Back: Piracy Statistics for 2023

[isubasinghe]

This is silly, it assumes people will purchase instead. I pirate stuff because I am bored and just want to watch something, my order of priorities are: Pirate, not watch, purchase.

On: Initiative to connect all European capitals through a high-speed train network

[isubasinghe]

Nah trains >>> planes, not even a comparison.

Especially since the cheaper plane flights in Europe are absolutely painful, dropping you off 2 hours away from the city centre into some minor airport.

Taking the TGV from Paris to Zuerich in comparison is such a relief.

On: Initiative to connect all European capitals through a high-speed train network

[isubasinghe]

meh apart from the Deutsche Bahn, I never had to wait around in Europe and I lived there for a year.

In a lot of ways, I understand why Deutsche Bahn sucks, a lot of politics ruined the company.

On: The Meltdown at CNN

[isubasinghe]

Al Jazeera (international) itself doesn't have any incentive to be biased, bias may obviously occur via journalist's opinions etc that creep in.

But as I understand, Al Jazeera is run as an means to show Qatar's importance/relevance.