1. 27

  2. 5
    1. 4

      This was a great talk, talks about proof languages are usually too high-level/academic for my small engineer brain, but I was able to follow this one without any problem. I wish there had been a comparison with Ada/Spark though as I’m unsure what ATS offers over these.

      1. 6

        I wrote a post comparing Ada/Spark and ATS in the area of proving program invariants if interested.

        1. 5

          Glad you liked it :)

          proof languages

          I wouldn’t necessarily call ATS a “proof language” just because you can do proofs in it. Much of your code would, realistically, not be proven correct. When you say “proof language”, I think of languages exclusively for mathematical proving, like e.g. HOL Light.