Formal software verification with AI: frontier AI produced SPARK…
www.adacore.com
See how AI wrote and proved SPARK Platinum code for AES, SHA-256 and HMAC from the NSA’s Cryptol specs, with no human guidance.
  • lobsters__frign@crustaceanson.theshelf.topM
    1·
    11 days ago

    Very impressive work! I always wondered in which way contract programming will move. This is one aspect where I see the human factor never being really phased out, because you need people to check the contracts. Ada/SPARK are languages that are just very nice to work with.

    I would like to encourage everyone to play around with them!

    score 1 · canonical