_______ __ _______
| | |.---.-..----.| |--..-----..----. | | |.-----..--.--.--..-----.
| || _ || __|| < | -__|| _| | || -__|| | | ||__ --|
|___|___||___._||____||__|__||_____||__| |__|____||_____||________||_____|
on Gopher (inofficial)
URI Visit Hacker News on the Web
COMMENT PAGE FOR:
URI Creusot helps you prove your Rust code is correct
Loic wrote 2 hours 1 min ago:
I like the name[0][1].
[0]: [1]:
URI [1]: https://www.britannica.com/place/Le-Creusot
URI [2]: https://en.wikipedia.org/wiki/Le_Creusot
Trung0246 wrote 2 hours 37 min ago:
How does this differ from
URI [1]: https://github.com/verus-lang/verus
rendaw wrote 2 hours 40 min ago:
I'm super interested in this sort of stuff, but I have a hard time
figuring out where to get started. Like, could this help in a typical
CRUD application? What sorts of problems is it super useful for? What's
a good way to get started integrating it into existing software, or is
it better to design software ground-up to be verified? Are there
limitations, or certain standard library features that are/aren't
supported?
(Not specifically for Creusot)
mbonnet wrote 2 hours 1 min ago:
A decent amount of mission-critical software undergoes formal
verification, like spacecraft flight software (my area of expertise).
SparkADA lives on because of not just its safety, but formal
verifiability.
crackalamoo wrote 45 min ago:
Interesting, how common is this vs just unit testing? How do you
avoid formally verifying something against a spec that could subtly
fail in production?
giltho wrote 3 hours 23 min ago:
Fantastic work
DIR <- back to front page