@janriemer
> former attempts with #Creusot and #Kani failed for me
How so?

🤩La ministre des Sports, Marie Barsacq, a salué l’action de l’Ufolep dans une vidéo diffusée lors de l’AG nationale Ufolep qui se déroulait au #Creusot les 26 et 27 avril derniers !

A découvrir dans la revue Enjeu Ufolep de mai 2025 n°66 👉 https://www.ufolep.org/?titre=ag-du-creusot--la-ministre-des-sports-salue-l-action-de-l-ufolep&mode=actualites&rubrique=0&id=168438

F* (fstar) Interactive Tutorial:

https://fstar-lang.org/tutorial/

I'm only like 10% into the tutorial, but this language is CRAZY (fun)! :awesome: 😄

I try to learn the fundamentals of it, so I can use the backend of it in #Aeneas... so I can ultimately formally verify my #Rust crate (former attempts with #Creusot and #Kani failed for me).

Aeneas:
https://github.com/AeneasVerif/aeneas

See part two of toot for a toy example of proving function equivalence

1/2

#FormalVerification #FunctionalProgramming #RustLang

Huh, seems like I really have been living on the bleeding edge (of #FormalVerification):

https://github.com/creusot-rs/creusot/discussions/1477#discussioncomment-12991148

The verification in the prev toot is currently not possible in #Creusot due to missing specs for the `Hash` trait and HashMap more broadly. 😔

Oh well, seems like (at least currently!) I won't be able to fully verify the diffing algorithm of #CSVDiff.🥺

Options I have now are:
- Only verify parts of the algorithm (that don't depend on HashMap ops)
or
- Use fuzzing/property testing

🚀 Le 26 avril, on construit l'avenir du sport UFOLEP au Creusot ! 🔥🏅

Santé & bien-être au cœur de l'AG Nationale : 3 ateliers interactifs sur santé globale, santé mentale et bien-être en club 💡

✨ Signatures majeures avec la MGEN et la CNAM 🤝 Rejoignez-nous pour un sport plus inclusif, éducatif et engagé ! 🎯 #ÉducationParLeSport #AGUfolep #SportPourToutes #Ufolep #EngagementAssociatif #Creusot #SaôneEtLoire

👉 https://tinyurl.com/2zxnzw97

🎉 Quatro au Creusot ! 🌟
À l’AG nationale UFOLEP, renouvellement de la signature du partenariat avec QUATRO, marque phare en équipements pour la gym artistique & trampoline 🤸‍♀️
👕 Justaucorps durables, designs performants : un style affirmé au service de toutes et tous.

📍 RDV les 26-27 avril au Creusot pour célébrer ce duo gagnant !

Plus d’infos sur : https://www.ufolep.org/?titre=assemblee-generale-ufolep-2025-au-creusot&mode=evenements&id=166290

#Ufolep #AGUfolep #SportPourToutes #ÉducationParLeSport #Creusot #saoneetloire #CNSGYM

Hm...I'm running into a timeout with #Creusot when trying to verify a simple `add` operation on a HashMap newtype 🤔

https://github.com/creusot-rs/creusot/discussions/1477

Does anyone have any idea what's going on here?

Disclaimer: I'm totally new to creusot and #FormalVerification, so please be gentle with me.😊

Boosts very much appreciated. :boost_love:

Thank you! ❤️

#IDontKnowWhatIamDoing #Help #FediHelp #FollowerPower #Rust #RustLang #Proof #Timeout

creuSAT - A formally verified #SAT solver written in #Rust and verified with #Creusot.

https://github.com/sarsko/CreuSAT

Mindblowing! 🤯

#FormalVerification #RustLang

Nice, I think I've found a (for me) suitable workaround for the above problem 👆 :awesome:

=> https://github.com/creusot-rs/creusot/issues/1337#issuecomment-2821430387

The "trick" is to use conditional compilation with `cfg` and `cfg_attr`, so we don't derive or use `Debug` when in context of Creusot.

See the above linked comment on how to do this exactly.

More on `cfg`, `cfg_attr` and conditional compilation in the #Rust reference:

https://doc.rust-lang.org/reference/conditional-compilation.html

#RustLang #Creusot #Bug #Workaround

Seems like I'm living on the bleeding edge of formal verification in #Rust!

Ouch! 😢 ⚔️ 🩸

=> https://github.com/creusot-rs/creusot/issues/1337#issuecomment-2819513924

#Creusot #RustLang #ICE #Bug

🎯 J-15 avant l’AG nationale Ufolep 2025 au Creusot !

🔔 Les 26 & 27 avril, débattons du futur du sport associatif & inclusif ! #Ufolep

💡 À ne pas manquer :
✅ Sport en ruralité : comment le rendre plus accessible ?
✅ Engagement & gouvernance : nouveaux défis, nouvelles perspectives 🔄
✅ Mayotte & Polynésie : solidarité & développement !
✅ Cap sur 2028 : le centenaire commence maintenant ! 🔥

#AGUfolep #SportPourToutes #EngagementAssociatif #Creusot

L’article juste ici 👉https://tinyurl.com/2zxnzw97

🏛️ Le Creusot accueille l’AG 2025 de l’Ufolep ! 📢

📅 26-27 avril 2025 | Centre universitaire Condorcet
Une AG au cœur d’un territoire engagé :
🏅 1 800 licencié·es, 33 associations
🏃‍♀️ Athlétisme, sports mécaniques, volley…
🤝 Initiatives inclusives : UfoBaby, UfoStreet…

💡 Un moment clé pour l’avenir du sport associatif !

📚 Lire l’article : https://tinyurl.com/2s3h6c5b

#AGUfolep #SportPourToutes #EngagementAssociatif #Creusot

#PhotoJanuary2025
Jour 13 : artificiel

Non vous n'avez pas été drogués à l'insu de votre plein gré : cette allée du parc de la Verrerie au #creusot arbore une #couleur tout ce qu'il y a de plus artificiel dans le cadre de jeux d'été 🪅
Ou comment voir la vie en rose alors qu'on est en train de vider l'appartement maternel 😬

21 septembre 2023

#photography #saonetloire

Une pensée pour un écrivain et poète qui a toujours vécu au #Creusot
. Un homme simple et abordable qu'on croisait en ville et avec qui on pouvait discuter.
Merci Monsieur Bobin...
😟

RT @TER_BFC_Trafic
N'oubliez pas les #GestesBarrières pour vous protéger & protéger les autres !

Voici le témoignage d'un de nos agent recueilli par @lejsl au #Creusot.