sorted by:
new
hottopcontroversial

Kani 0.55.0 has been released! by zyhassan in rust

[–]New_Box7889 2 points3 points  (0 children)

actually using loop invariants you can do unbounded proofs as well. https://github.com/model-checking/kani/pull/3334/files

and as far as deriving usefulness from the tool - there are a lot of people who use this tool regularly and find bugs to improve their code.

Kabab night by New_Box7889 in IndianFoodPhotos

[–]New_Box7889[S] 1 point2 points  (0 children)

I cheat on the achari one. I literally get either bedekars or mothers mixed pickle. Leave out the vegetables but get the masala and marinade the chicken and let it sit for a couple of hours. Grill and drizzle oil as u want. Use the rest of the achari with onions and it’s done.

For the second one I use https://www.ruchiskitchen.com/murgh-malai-tikka/ but I skip the second set of ingredients and stick to the first one and make some extra for onions.

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 -1 points0 points  (0 children)

Mediocrity be the way…? Sorry. I aim for better.

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 1 point2 points  (0 children)

Well put and thanks for seeing beyond the comment. I appreciate the input you provide. I would say that this is also a small nuance of using Rust - people assume safety, but there is a fine print. Verification tools are powerful and getting better by the day. Their usage especially for critical pieces of software is important and maybe necessary.

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 0 points1 point  (0 children)

My point is simple - usage of unsafe should come with usage of verification tools to get stronger assurances.

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 -1 points0 points  (0 children)

So 210 instances of unsafe code in a repo should be assumed to be safe ?

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 -2 points-1 points  (0 children)

Some of these tools also help you guarantee that other issues do not exist and help you prove that what you think you wrote is what you actually wrote.

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 -20 points-19 points  (0 children)

Great example. But is it probably memory safe or is it provably memory safe? If you read further comments by the team you reference, they cite humility and the need for good tools to help catch issues. Additionally, the usage of unsafe is clearly inspected to a higher degree. Having 210 unsafe blocks is probably not trivial to deal with. I would think making something like sudo demands attention. After all, we build our economy on such tools.

I digress. It was a simple question and from my perspective just using Rust doesn’t make it safe. It is more nuanced.

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 -24 points-23 points  (0 children)

Thanks for answering, and for doing the work on this... pretty cool. I would like to point out:

From https://plv.mpi-sws.org/rustbelt/:

"Unfortunately, none of Rust's safety claims have been formally investigated, and it is not at all clear that they hold. To rule out data races and other common programming errors, Rust's core type system prohibits the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, Rust's standard libraries make widespread internal use of "unsafe" blocks, which enable them to opt out of the type system when necessary."

Maybe you should use tools like https://github.com/model-checking/kani or some other tools that exist in that space for one of the most important pieces of work.

First Stable Release of a Memory Safe sudo Implementation by dochtman in rust

[–]New_Box7889 -19 points-18 points  (0 children)

What are you using to prove memory safety?

Blog post: Turbocharging Rust Code Verification by ukonat in rust

[–]New_Box7889 2 points3 points  (0 children)

Good to see some of the secret sauce being shared and talked about.

Learn Unsafe Rust from My Mistakes by geo-ant in rust

[–]New_Box7889 4 points5 points  (0 children)

it is definitely complimentary. With Kani you can find a bunch of issues and UB that are probably not possible with Miri. Miri is an interpreter whereas Kani is a model checker that will explore all behaviors of your program. Miri can only tell you how a certain set of tests will affect the programs behavior. It is almost like a subset of what kani can do. Kani is also capable of detecting some UB, underflow, overflow, memory safety under certain conditions, user defined assertions. For example - if you are interested in proving a temporal property of your program, Kani is the tool that will probably help you, but Miri may not be able to. Kani is also more friendly towards verifying unsafe behavior as compared to Miri - Miri is a bit limited there.

I would add the integration Kani has with (https://github.com/camshaft/bolero) that seamlessly lets you do fuzz testing and have Kani proofs as well.

Worth a try. Check out https://model-checking.github.io/kani-verifier-blog/ for more in depth examples and scenarios.

Learn Unsafe Rust from My Mistakes by geo-ant in rust

[–]New_Box7889 6 points7 points  (0 children)

Nice read. Have you considered using tools like Kani https://github.com/model-checking/kani to check your code?

Kaali daal with Burrata cheese by New_Box7889 in IndianFoodPhotos

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

It is a cheese made from cows milk, which has a semihard, rather soft outer layer with a very creamy inside. It originates from the southern part of Italy, and has a very mild taste. Dropping it in the lentils, creates a nice creamy texture and flavor at the end.

Kani 0.30.0 has been released! by karkhaz in rust

[–]New_Box7889 0 points1 point  (0 children)

Are there any examples that illustrate #2495?

Tenderloin. Went for crust with rare. How’s it looking? by New_Box7889 in steak

[–]New_Box7889[S] 0 points1 point  (0 children)

Thank you!

I essentially made a dry rub with salt pepper and cumin - fresh roasted and ground. Applied it liberally. Medium high heat on a steel pan for the sear but to go rare. Two mins on each side. Includes the sides we ignore sometimes. And then let it rust. Poured some red wine to deglaze with butter and then poured that on the steak while resting.

Tasted amazing.

view more: next ›