type safe high assurance practices in haskell, agda, the heterogeneous tool set, intuitionistic type theory, constructive logic and java 8