Driving with D - Hackdot

Re:Driving with D by gavinray on Tuesday June 01, 2021 @01:13PM (#27357934)

There are some things that attempt to come close. Prusti by ETH Zurich is maybe the closest.

https://github.com/viperproject/prusti-dev

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.

[ Parent | on HN ]

Re:Driving with D by eggy on Tuesday June 01, 2021 @09:21PM (#27363674)

I 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.

[ Parent | on HN ]