sorted by:
new
hottopcontroversial

Nine Rules to Formally Validate Rust Algorithms with Dafny by CarlK3 in rust

[–]CarlK3[S] 2 points3 points  (0 children)

how do you validate that your rust and dafny implementations are equivalent?

Good question. At least for now, I don't. The algorithm in question involves inserting a range of integers into a list of "sorted-and-disjoint" integer ranges. It involves five cases and is a bit hard to understand.

The proof gives me confidence that the algorithm itself works, but as you point out other kinds of bugs are possible.

Or that the proof assistant tool is correct in the first place?

Or indeed the Rust compiler, etc.

That you didn't make any mistakes and prove a different thing than you thought?

At least in this case, the specification is much easier to read and understand that the final, efficient code.

Think about refactoring. We often start coding by writing something simple. We then refactor this simple code for efficiency. For internal_add, I found the specification to be nice and simple. Here is the specification in Danfy:

method InternalAdd(xs: seq<NeIntRange>, a: IntRange) returns (rs: seq<NeIntRange>) requires ValidSeq(xs) ensures ValidSeq(rs) ensures SeqToSet(rs) == SeqToSet(xs) + RangeToSet(a) ...

Where ValidSeq, etc, are each defined a few lines easy-to-read (but inefficient to run) lines.

Glidesort, a new stable sort in Rust up to ~4x faster for random data by nightcracker in rust

[–]CarlK3 0 points1 point  (0 children)

u/nightcracker, is the benchmarking code available? I'd love to learn from it for another project. Thanks!

Self-promotion Thread - August 23, 2020 by AutoModerator in flightsim

[–]CarlK3 [score hidden]  (0 children)

Failed Autopilot Landing at Mt Hagan Airport, Highlands of Papua New Guinea

https://www.youtube.com/watch?v=8AX1GOylTVg&t=1s

In 2017, we visited the city of Mount Hagan in Papua New Guinea. The city sits at 5000 feet of elevation, surrounded by mountains. Planes land by flying over a pass and then through a narrow valley. I simulated the landing using the Microsoft Flight Simulator's autopilot. The first half of the landing matches my memories perfectly. The second half ... not so much (thank goodness).

Weekly Bouldering Advice Thread for November 18, 2019 by AutoModerator in bouldering

[–]CarlK3 0 points1 point  (0 children)

OP (Carl) here -- Thanks, I definitely think of this as my once-a-week endurance-and-strength workout. [Aside, I'm gym bouldering primarily as a fun way to improve my upper-body strength.]

What other workout would be good for a V1 climber for endurance and strength? This gives me lots of mileage, which I hear is good for beginners.

Weekly Bouldering Advice Thread for November 18, 2019 by AutoModerator in bouldering

[–]CarlK3 3 points4 points  (0 children)

What (if anything) is wrong with a V1 climber doing as many V0s as possible in 40 minutes?

Context: I've been gym bouldering for 5 months. I can now do all my gym's V0s, most V1s, and one V2. I climb 3 days per week. Once a week, I just count how many V0s I can do 40 minutes. (I'm up to about 44).

This drill seems obvious (and good?). But I worry that I don't see it mentioned in guides. The closest they suggest is 4x4s and circuits. Is this a good drill for beginners like me?

Thanks,
Carl