Having also written lots of code with nothing but Tests as the Functional Spec I'm not sufficiently familiar with Formal Methods, though I should make myself learn. TIL that there are different tools for Design/Implementation/Verification instead of just code and decorators and IDK annotations as decorators and autocorrect.
(TODO: link to post about university-level FM programs)
Always wondered whether there's some advantage to translating to another language's AST for static and/or dynamic analysis or not. AFAIU Fuzzing is still necessary even given Formal Implementation?
Python is Turing complete, but does [TLA,] need to be? Is there an in-Python syntax that can be expanded in place by tooling for pretty diffs; How much overlap between existing runtime check DbC decorators and these modeling primitives and feature extraction transforms should there be? (In order to: minimize cognitive overload for human review; sufficiently describe the domains, ranges, complexity costs, inconstant timings, and the necessary and also the possible outcomes given concurrency,)
(TODO: link to post about university-level FM programs)
Always wondered whether there's some advantage to translating to another language's AST for static and/or dynamic analysis or not. AFAIU Fuzzing is still necessary even given Formal Implementation?
Python is Turing complete, but does [TLA,] need to be? Is there an in-Python syntax that can be expanded in place by tooling for pretty diffs; How much overlap between existing runtime check DbC decorators and these modeling primitives and feature extraction transforms should there be? (In order to: minimize cognitive overload for human review; sufficiently describe the domains, ranges, complexity costs, inconstant timings, and the necessary and also the possible outcomes given concurrency,)
"FaCT: A DSL for Timing-Sensitive Computation" and side channels https://www.hackerneue.com/item?id=38527663