On 3 March 2014 16:33, Martin Decky <[email protected]> wrote: > > By the way, I expect an argument of the form that the static type should >> not depend on complicated analysis of condition expressions. I agree. >> You can, however, only interpret for type annotations a certain form of >> expressions, put those expressions in there as assertions, and let the >> SMT solver prove (or disprove, or timeout for) the rest. >> > > Yes, but the concern that remains is that the SMT solver might timeout in > many non-trivial cases. To what extent should the core language rely the > SMT solver and to what extent should be easier formal verification only a > bonus. > > My opinion is that the compiler should report any assumptions and preconditions it can't prove (quickly), without stopping the build. It would be up to the developer to either ignore the report, or refactor the code/conditions appropriately. In the worst case, you have an explicit list of claims you expect to be true, which is still much better than most languages.
-- Jirka Z.
_______________________________________________ HelenOS-devel mailing list [email protected] http://lists.modry.cz/listinfo/helenos-devel
