3 ms·

I have found Isabelle very useful, and Dafny even more so. Amazon AWS uses Dafny to prove the correctness of some complex components. Then, they extract verif

by nextos 11mo ago

I have found Isabelle very useful, and Dafny even more so. Amazon AWS uses Dafny to prove the correctness of some complex components. Then, they extract verified Java code. There are other target languages. Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.

kragen 11mo ago
Have you tried using them as macro assemblers in the way described in the paper?
- nextos 11mo ago
  No, I haven't. I have used them with shallow embedding techniques that are relatively similar, but not in this way.
  - kragen 11mo ago
    That sounds interesting!