Rust Get a BBL: Addressing Your Comments

Quick follow-up to last week's Creusot video.

You had great feedback. Let me address the main points:

TIMESTAMPS
0:00 - Intro & Holiday Greetings
0:28 - Ada/SPARK Comment ("Learn Ada")
1:41 - Safe Rust & UB Clarification
3:10 - "Just Use Result" Discussion
3:45 - Compile Time Reality
4:25 - Clippy Lints
5:05 - Closing & Takeaways

KEY POINTS ADDRESSED:

1. Ada/SPARK History
Yes, Ada/SPARK has been doing this since 1983. Eiffel since 1986.
This video is about Rust specifically - like Frama-C is for C.

2. UB vs Panic
I misspoke: safe Rust panics are NOT undefined behavior.
They're defined, controlled crashes.
Thanks @dernett for the correction.

3. Why Not Just Result?
Result is perfect for error handling.
But doesn't prove algorithm correctness.
Binary search can return Result and still have bugs.

4. Compile Times
Yes, formal verification is slow.
Use it when bugs are MORE expensive than verification.

COMMENT CREDITS:
@kamertonaudiophileplayer847 - Ada/SPARK history
@dernett - UB vs panic precision
@AliceTurner-q3f - bounds checking clarity
@MaestroBauxSplinter - Result vs proofs
@shakkar23 - compile time reality
@romanstingler435 - Clippy lints

RESOURCES:
Original Creusot video: https://youtu.be/[REPLACE_WITH_PART1_LINK]
Ada/SPARK: https://adacore.com/about-spark
Frama-C: https://frama-c.com
Creusot: https://github.com/xldenis/creusot
Dafny: https://dafny.org

#rust #Creusot #FormalVerification #Ada #SPARK #Programming
#c #cpp #dafny #testing #Programming, #SoftwareEngineering, #reaction #systemdesign #coding #computerscience