| /* | |
| * The following example code demonstrates how Kotlin's type system violates | |
| * a conventional property of type systems, Subject Reduction. The Kotlin type | |
| * system is therefore not "safe" according to the conventional notion in | |
| * programming languages theory. See the code in the `main` function below. | |
| * | |
| * This notion of type safety relies on a reduction semantics for the | |
| * language, which Kotlin doesn't purport to implement. However, any | |
| * reasonable language's operational semantics would contain a rule like | |
| * `f(e_arg)` evaluates to `e_body[e_arg/x]` when `f(x) = e_body` is the |
import ReadWorlds
ctx <- buildCtx "<cabal-sandbox-path>" ["base", "containers"]
printCtx ["Prelude", "Data.Map"] ctx
I hereby claim:
To claim this, I am signing this object:
| (* Here is some client code that needs to | |
| construct a proof about fac. Because it doesn't | |
| rely on any particular *representation* of | |
| nats, it imports the abstract nat interface; | |
| thus it could be linked against Peano, binary, | |
| and other implementations of the nat interface. *) | |
| (* Assume 'Nat' refers to the abstract spec, NatSpec. *) | |
| Import Nat |