I always thought critical applications like banking needed compile time type checking. Clojure is neat and all, but it's dynamic.
https://github.com/Prismatic/schema
https://github.com/clojure/core.typed
These are both libraries that you can choose to use. Both Typed Clojure and Schema are more powerful than Java's type system. By powerful I mean you can declare types and constraints that aren't expressible in most type systems (eg: an object can not be NULL, or a Map or Array must have specific keys or type'd values). Schema is run-time (we only leverage it in development and testing), while Typed Clojure is more akin to compile time.
Is that fair?
Hmm. Can it do anything better than that?
Java has optional nullity annotations that tools like Findbugs and (more usefully) IntelliJ can use to highlight nullity bugs. Kotlin has nullity integrated into the language's type system in a much better way. Stating that a Map or Array must have specific types in it is the whole purpose of generics, which Java had since 1.5, no?
Don't get me wrong. The Java type system is not that strong and has some frustrating holes in it. But typed arrays and nullity tracking doesn't seem like some advanced Clojure-only tech, to me.
Wrt the typing of Maps and Arrays, what Clojure supports goes way beyond what Java's type system supports: you can specify that the first element of an array has to be of type X, the second is of type Y, the third can be either NULL or Z. For maps, you can specify that a key must have a particular type and must be in the map, with a specific value while other keys may be present (required or not) and you can compose any of the constraints mentioned on the values the keys may take.
This is different from Generics in that Generics constrain to homogeneity for an entire collection.
You could create formal objects in your Java code to express similar constraints, but you're not achieving the same result: a Java object actually has the property (even if it's null) while a map (or an array) with an optional member will only have it if it's present. With Java you'd need many classes to model all the specific combinations. Java's current type system is significantly less expressive and doesn't have the same power. I realize those are subjective. By expressive and power I am referring to whether you can declare an idea in your code or whether you have to write the imperative logic to implement an idea (the former meeting my definition of expression or power).
Thanks for the question.
Quickly you discover you need a type system. (I'm not familiar with Kotlin but I'm sure it's fine.)
The answer is that core.typed's type system is proper space-age tech, but it's also not exactly ready for production use.
They need quality, trustworthy software. Compile time type checking is a tool that can be used to help get there (but how useful it is in getting there depends on how robust the type system is, and Java's is not particularly robust).
Clear and concise code that is readily understood, avoids visual noise so that the programmer can focus on function, also is a tool that can help with that.
Clojure focuses more on the latter than the former, but that doesn't necessarily make it worse, and may make it better.
To be clear, I'm not suggesting that Clojure is a bad language. I really enjoy using Lisp-like languages! I also enjoy modern statically typed languages (and on balance prefer them). My experience is that having good people and avoiding bad technology choices (e.g. choosing Ruby for high throughput and low latency environments) is the secret to success. Stories like these are invariably sold as technology successes (and, equally, technology is blamed when things go bad.) I believe the reality is more that better technology attracts better people. It's the better people and chance to avoid legacy that gives success.
So when you watch cat videos on your smart phone, there is about 50% some non-statically compiled functional code has done its job in setting up the necessary signaling.
WhatsApp has also recently been the poster child for running a successful distributed platform, with a tiny number of engineers (about 10 or 20) by also leveraging a non-statically compiled and functional language.
In general static type checking is nice, I like it. But clearly not a deal breaker. O often hear "I won't touch anything unless it has static typing" or "large applications should have static types".
But maybe the question to ask, should applications be that large? Lately we have been all upvoting microservices. And if anything those encourage decoupling large monstrous application into smaller independent services. At that point there are just a soup of dynamically typed components.
I ask this because I've been eager to get my hands dirty with Clojure. I have experience with other functional languages (Haskell, OCaml, F# and some Emacs Lisp), so the paradigm isn't new.
I've looked at core.typed, but doesn't seem as neat as the syntax of Typed Racket. It's something, though. Is it checked at compile time?
What irks me is that static typing and type inference can make code feel really robust, and for the lack of a better word, safe. In Clojure I see a lot of nice things but the lack of typing, though common for Lisps, always bothers me a bit. I don't like runtime errors that happen because the compiler wasn't able to tell me that this object doesn't have that method. JavaScript's undefined is not a function or its kin in Python are examples of this behaviour, which I don't like.
Though, I see that Clojure's answer to this is rapid REPL development--which is great!--and unit testing, and what I've recently discovered, pre- and post-conditions. But it still feels somehow inferior.
I am torn between learning Scala or Clojure. Knowing OCaml and F#, Scala doesn't look that interesting, messy and multi-paradigm. Clojure appeals to me because its a Lisp and has one paradigm, but on the other hand I'm scared by runtime exceptions.
Should I just ignore my trepidations and proceed?
Yap give it a try.
From what I understand Core.typed while not as rigorous as static type system in Haskell or OCaml can let you gradually add typing to your application. They more you add the greater the benefit.
But also personally haven't used it.
I used Dialyzer in Erlang, which is a similar concept. You annotate your code with types and the more you do the more type errors it will find for you:
http://learnyousomeerlang.com/dialyzer
It is surprisingly good. Here is example of production code in Erlang with some type annotations (it is a websocket handler from Cowboy a webserver):
https://github.com/ninenines/cowboy/blob/master/src/cowboy_w...
Notice the type and -callback declarations at the top then the -spec lines before some functions.
While they may have a small number of engineers (20 or max 20?), their engineers are probably laser focus in delivering the product (re: no web-app for the longest of time, no RoR vs Django vs Clojure vs Java vs PHP, no React vs Backbone vs etc etc), just back-end: Erlang, front-end: various phones that needed to be supported.
I would attribute their success at their skill set and experience. If you watch Rick Reed presentation in MeetBSD, a few key points to note: Rick Reed is very smart and knows full-stack (minus the browser): from the OS (internal, driver, etc) up all the way to Erlang VM and the WhatsApp backend.
The team had to modify FreeBSD and patch Erlang VM whenever necessary. How many companies have _that_ kind of talent? (e.g.: modify Linux and JVM to make them run faster? or Ruby implementation and PostgreSQL/MySQL while supporting the actual product?). Rick himself has tons of experience writing distributed systems at Yahoo! (using C++ nonetheless...).
While Erlang helps them but in reality, their skill + experience matter more.
While Clojure is a dynamic language, it actually does have optional type checking, courtesy of the core.typed library. This isn't perfect, but it is considerably more sophisticated than Java's inbuilt type system.
Even without static type checking, I'd argue that Clojure is the safer language by default, since it mostly avoids mutability.
> Here are some specifics – our new code is going to be an order of magnitude less in volume than the old and this is being conservative.
Java's static typing would help catch mistakes but it's not magic. And by moving this piece of their system to Clojure, they've managed to simplify it so much that there's much less room for mistakes to hide.
We could have done it in a week with rails scaffolding capabilities and the vast gem environment, but we are doing everything manually in Scala, because type safety and performance. It's so frustrating that I'm looking forward to quit very soon.
The fact that Rails has scaffolding and whatever Scala framework your team uses doesn't has little to do with type safety (there are plenty of web frameworks in dynamic languages without scaffolding as well).
There are several languages which require a comparable amount of typing to a dynamic program, while adding considerable type safety.
I really despise the "let's finish this in one week" that is typically going on for me. I'd rather learn best practices, even if they're in a language, and have some experience building long-lasting services.
Feels like the difference in working at a mobile home shop vs a custom log home company.
Except 5 years later, when the happy developers have gone on to express themselves elsewhere, and left behind them a mess. Now, you can make a mess in any language, but a mess in a dynamic language is considerably harder to refactor.
I also dispute the claim that a strong type system is a "tiny factor" in code quality. Being able to express invariants with types makes code much robust, and self-documenting.
There actually are some studies that show that using a static typing system is only a tiny factor when it comes to code quality:
http://wadler.blogspot.co.uk/2011/09/experiment-about-static...
However, I've also read studies that show the opposite, but the lack of rigurosity and the possible confounds that show up for both sides seems to render this as an open question.
This doesn't look particularly convincing, indeed (though studies about programming languages rarely are).
Hopefully they had tests. And unless they've mathematically proved the code always does what it expects (I've only seen that in avionics systems).
Also depends on application of course. Large concurrent and distributed applications benefit a bit less from static typing in traditional languages. Or rather, they are so hard, that type error are not as much of a significance. How concurrency, communication and failure is handled is more critical.
But say a game or a large desktop application with millions of lines of code, could get a larger benefit from static type checking, no doubt.
Now for a bit of personal experience. I have programmed in Java, C#, Python, Erlang, C++. I have found that when working with large or unknown code bases C# for example is great. Just having the IDE and generics support in C# during compile time is awesome. But if I program something from scratch, I can make a lot faster progress in Python. I often put more work into both unit tests and integration tests because I just have more time available.
Also failures during run-time, even in Python, in my systems a very rarely type errors (those are caught pretty early one). But they are often logic or concurrency errors.
If you use them right, expressing the constraints of your system in the type system, you can improve huge areas of quality. It doesn't give you much for free, but it does give you a tool that lets you check your own correctness properties more efficiently and maintainably than any alternative.
> Lack of expressiveness or lack of developer happiness can be much more detrimental to software quality than lack of static typing.
Agreed - but good static typing makes a language more expressive, not less.
Not to say they don't use Java as well various other languages, but right tool for the job...
Bank of America was supposed to have gotten heavily into Python a couple of years (or more) ago. I had blogged about it here at the time:
http://jugad2.blogspot.in/2013/10/bank-of-america-to-rebuild...
and Niall O'Connor from the bank (who spoke at PyCon IE 2013 - http://python.ie/pycon/2013/speakers/niall_oconnor/ ) confirmed via a comment on my post, that they were not "beginning" to do it, but that it had "already happened".
Edit: The reddit thread quoted by the parent comment, also mentions BoA and Niall.
And the whole system is in part credited with helping them survive the recent financial crisis ... although simply listening to their risk people was more important. But it's all intertwingled, I'm sure, because good risk people would want a system like SecDB so they know the company's positions in quasi-real time with a great deal of assurance vs. hours and days and through e.g. scraping spreadsheets, often manually, etc.
With contractual based programming, pre/post assertions, schema validation, etc... you can add all the type checking you want. That along with the other well known benefits of functional programming I think would make it highly desirable to build large complex systems in.
If a banking program fails, they can just ask for a mulligan from the central bank/government. They're just playing with people's life savings, not any actual lives, right?
If they're going to suck up all the best brains in the industry anyway, they ought to be able to do SPARK/Ada.
If I were making banking/trading software, I'd start with an OS that combined the security paranoia of OpenBSD with the deterministic performance of LynxOS, build some tools that validate source code by automated proof rather than testing, and hire a bunch of people smarter than me to build software that is secure, reliable, and profitable, in that order. No bank in existence would be crazy enough to pay me to try.
For a "bank bank", "playing with people's life savings", the lower level transnational stuff, yeah. Although I don't get the impression that the current stuff doing that is prone to disastrous failures, and I believe the system has some slack here and there to reverse errors, i.e. transfers of money vs. buying and selling financial instruments. The current infamous failure in this area, which was WRT to the latter, was at Knight Capital.
But above a certain level, at which point we're not so much "playing with people's life savings" (or, rather, if they have a clue, only a small portion of them), the situation can be a lot more fluid. E.g. changing trading strategies, which can be driven by the capriciousness of governments. The current state of the art doesn't make it practical to embed the US tax code into source code amenable to automated proof, especially before it changes again, right??
It's incomplete, but here is where I'm gathering the data: https://github.com/steveshogren/blog-source/blob/master/sour...