Does anyone have an estimate to the difficulty of using Dafny as an annotation to programs written in another programming language? I'm thinking of one on a dif

Does anyone have an estimate to the difficulty of using Dafny as an annotation to programs written in another programming language? I'm thinking of one on a different OS (Linux) than the MS Windows OS for which Dafny appears to be written.