3 ms·
There are some things that attempt to come close. Prusti by ETH Zurich is maybe the closest. https://github.com/viperproject/prusti-dev https://github.com/vipe
by gavinray 5y ago
There are some things that attempt to come close.
Prusti by ETH Zurich is maybe the closest.
https://github.com/viperproject/prusti-dev https://github.com/viperproject/prusti-dev
https://www.pm.inf.ethz.ch/research/prusti.html https://www.pm.inf.ethz.ch/research/prusti.html
extern crate prusti_contracts;
use prusti_contracts::*;
#[requires(something)]
#[ensures(result >= a && result >= b)]
#[ensures(result == a || result == b)]
fn max(a: i32, b: i32) -> i32 {
if a > b {
a
} else {
b
}
}
Ada seems like a fantastic language though, and the 202x edition brought some niceties to the language.
- eggy 5y agoI am an Ada/SPARK novice, but on first look Prusti seems to deal with contracts, but I am not sure how much more of the Ada/SPARK system it may covergg. I used to dislike Ada and SPARK due to their verbosity, but after studying some of the embedded work in them, and what they bring to the table, I am no longer put off by that or syntax. I've seen Julia and even Elixir projects in areas that would better suit Ada/SPARK, but I think it is due to their popularity rather than applicability. But things like Elixir's Nerves platform is very interesting in bringing the BEAM to the embedded world, and I love Pluto notebooks for Julia, but for high-integrity software I think I'll try and leverage Ada/SPARK's capabilities and pedigree for now. I will look further into Prusti this weekend.