skilpat

(* 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

skilpat

Keybase proof

I hereby claim:

• I am skilpat on github.
• I am skilpat (https://keybase.io/skilpat) on keybase.
• I have a public key whose fingerprint is 08A0 1014 F958 24D7 D360 B2E5 A954 3B6F 48DD BBF3

To claim this, I am signing this object:

skilpat

Instances visible in various Haskell modules

• Haskell implementation: ghc-7.8.4
• All other packages: LTS Haskell 2.3 from Stackage
• Calculated using the code at https://github.com/skilpat/class-struggle

import ReadWorlds
ctx <- buildCtx "<cabal-sandbox-path>" ["base", "containers"]
printCtx ["Prelude", "Data.Map"] ctx

skilpat

/*
 * 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