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?
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.
I like the name[0][1].
[0]: https://www.britannica.com/place/Le-Creusot
[1]: https://en.wikipedia.org/wiki/Le_Creusot
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)
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.
How does this differ from https://github.com/verus-lang/verus
Fantastic work