To be able to prove any "interesting" properties in our language, we'll quickly run into the need for tactics -- writing proof objects by hand is just too cumbersome! An interesting question would be whether the tactic language is extensible, or if the allowed tactics are provided by the language runtime (our Haskell implementation).
To be able to prove any "interesting" properties in our language, we'll quickly run into the need for tactics -- writing proof objects by hand is just too cumbersome! An interesting question would be whether the tactic language is extensible, or if the allowed tactics are provided by the language runtime (our Haskell implementation).