As I mentioned in my earlier post I do not think it is the power of the type system that is key but its consistency and the accompanying tools. I am not saying

As I mentioned in my earlier post I do not think it is the power of the type system that is key but its consistency and the accompanying tools. I am not saying programming in Coq or dependent types are the answer. I am asking, what if programmers had access to a more polished toolkit to create domain specific versions of djinn where it would guide them or help layout some basics? Knowing that the code was derived from sound axioms. Other engineers can quickly protoype the validity of their ideas by mechanically running through some equations, why not software engineers? Already I use types in Haskell and F# to help me figure out how to layout the code - I write some basic code where I know which function it will feed into, I don't have to think much as I try to get the code to fit the types. Nothing fancy but still highly useful. As for code transformation I don't mean generic stuff like Visual Basic to Java, I mean having a team able to write the tools themselves with full awareness of the requisite semantic mappings. Or even better, creating a dsl for the domain and then having that map down to appropriate platform specific code. But it need not be traditional development you could extend it to machine learning - say you are doing genetic programming to fit data, using types to have some level of axiomatic reasoning rather than random cross over may be fruitful. There are all sorts of uses where application of basic - not fancy theory is helpful.