Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
en.osm.town is one of the many independent Mastodon servers you can use to participate in the fediverse.
An independent, community of OpenStreetMap people on the Fediverse/Mastodon. Funding graciously provided by the OpenStreetMap Foundation.

Administered by:

Server stats:

258
active users

en.osm.town: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.8

#creusot

1 post1 participant0 posts today
Jan :rust: :ferris:<p>F* (fstar) Interactive Tutorial:</p><p><a href="https://fstar-lang.org/tutorial/" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">fstar-lang.org/tutorial/</span><span class="invisible"></span></a></p><p>I'm only like 10% into the tutorial, but this language is CRAZY (fun)! :awesome: 😄 </p><p>I try to learn the fundamentals of it, so I can use the backend of it in <a href="https://floss.social/tags/Aeneas" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Aeneas</span></a>... so I can ultimately formally verify my <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rust</span></a> crate (former attempts with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Creusot</span></a> and <a href="https://floss.social/tags/Kani" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Kani</span></a> failed for me).</p><p>Aeneas:<br><a href="https://github.com/AeneasVerif/aeneas" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">github.com/AeneasVerif/aeneas</span><span class="invisible"></span></a></p><p>See part two of toot for a toy example of proving function equivalence</p><p>1/2</p><p><a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://floss.social/tags/FunctionalProgramming" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FunctionalProgramming</span></a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RustLang</span></a></p>
Jan :rust: :ferris:<p>Hm...I'm running into a timeout with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Creusot</span></a> when trying to verify a simple `add` operation on a HashMap newtype 🤔 </p><p><a href="https://github.com/creusot-rs/creusot/discussions/1477" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">github.com/creusot-rs/creusot/</span><span class="invisible">discussions/1477</span></a></p><p>Does anyone have any idea what's going on here?</p><p>Disclaimer: I'm totally new to creusot and <a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a>, so please be gentle with me.😊 </p><p>Boosts very much appreciated. :boost_love: </p><p>Thank you! ❤️ </p><p><a href="https://floss.social/tags/IDontKnowWhatIamDoing" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>IDontKnowWhatIamDoing</span></a> <a href="https://floss.social/tags/Help" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Help</span></a> <a href="https://floss.social/tags/FediHelp" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FediHelp</span></a> <a href="https://floss.social/tags/FollowerPower" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FollowerPower</span></a> <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rust</span></a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RustLang</span></a> <a href="https://floss.social/tags/Proof" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Proof</span></a> <a href="https://floss.social/tags/Timeout" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Timeout</span></a></p>
Jan :rust: :ferris:<p>creuSAT - A formally verified <a href="https://floss.social/tags/SAT" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>SAT</span></a> solver written in <a href="https://floss.social/tags/Rust" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Rust</span></a> and verified with <a href="https://floss.social/tags/Creusot" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>Creusot</span></a>.</p><p><a href="https://github.com/sarsko/CreuSAT" rel="nofollow noopener noreferrer" translate="no" target="_blank"><span class="invisible">https://</span><span class="">github.com/sarsko/CreuSAT</span><span class="invisible"></span></a></p><p>Mindblowing! 🤯 </p><p><a href="https://floss.social/tags/FormalVerification" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>FormalVerification</span></a> <a href="https://floss.social/tags/RustLang" class="mention hashtag" rel="nofollow noopener noreferrer" target="_blank">#<span>RustLang</span></a></p>
ExploreLive feeds
About