HN Theater @HNTheaterMonth

That's not empirical evidence that formal methods are more effective than other approaches. It just shows that the culture at these companies is conductive to using them. Walmart https://www.youtube.com/watch?v=av9Xi6CNqq4 and Boeing https://www.youtube.com/watch?v=iUC7noGU1mQ etc use different approaches. :)

⬐ skrishnamurthi

You claimed "There's absolutely no evidence that formal methods approaches are effective in practice." and said the only real use was for compilers. I pointed out that they are effective in practice in domains completely unrelated to compilers. Your response is to bring up a totally different point ("more effective than other approaches" — a statement that can't even be falsified), talk mumbo about "culture", and point to Clojure talks, which is neither here nor there. In short, you are perfectly suited for "conversations" on the Web.

⬐ yogthos

How do you define effectiveness? A company using a particular approach does not automatically imply that it's an effective way to do it. You can make any approach work if you invest enough resources into it.

To determine whether a particular approach is effective, it has to be compared against the available alternatives to determine whether it's effective or not. So, I'm a bit baffled by you saying that's a totally different point.

So, perhaps you can explain the metric that you're using here to define effectiveness.

Amazon was specifically using Clojure for the online checkout system, and the team bragged a few years ago how the system survived black friday without a hickup.

Walmart is using Clojure for their checkouts as well https://www.youtube.com/watch?v=av9Xi6CNqq4

Boeing is using it in the onboard control systems for the 737 Max https://www.youtube.com/watch?v=iUC7noGU1mQ

It's not some obscure microservice that some intern wrote over the weekend, these companies are using the language for critical applications, and the feedback from these companies is positive.

⬐ taloft

The Boeing video says Clojure is used for maintenance systems, not control systems. That’s an important distinction. Maintenance systems can go offline and the aircraft still flies fine. The critical control software is not written in Clojure from what I could tell.

⬐ hellofunk

Critical software is rarely written in anything except languages with explicit memory control, usually C++, and usually with very strict guides. There is a famous programming guide for flight control systems in particular that discusses how to properly use C++ for maximum safety during flight. It includes things like never allocating memory after take-off.

You wouldn't want Clojure, Java or any languauge with GC running in a pacemaker either. Those are all also very important distinctions.

⬐ user5994461

The majority of critical software is C, sometimes it's C++ or Ada instead.

C++ actually proved difficult to adopt over C. The language is too difficult and the tooling is too poor. It's too hard to run a static analysis or prove 100% code coverage.

⬐ hellofunk

I'm not sure what your evidence is for this, but I find C++ to be used far more widely than C in nearly all the companies I interact with that do critical low level work. And there is indeed plenty of information in the industry about flight control software in particular in C++. It's also very popular for embedded work, because C++ allows you to offload quite a bit of work to compile time that can only be done in C at runtime. And I've attended talks for security systems in C++ specifically because of control over exceptions and how to track unexpected events, which is something security professionals are very interested in.

With regards to tooling, the windows visual studio experience for C++ is widely counted as one of the best development setups in the industry for any language. I know lots of people working in other languages that envy what C++ developers get.

⬐ darksaints

The online checkout system isn’t a single service. I personally worked with the Delivery Promise service for a short time, and that service was composed of 8 different services...and that was just to calculate when we promised arrival to the customer during checkout. As in, they were just a single component of hundreds called during checkout. At the very least, none of those 9 services used Clojure.

If anybody led you to believe that their team did “online checkout”, but didn’t care to explain how small of a cog they were in an extremely complex system composed of hundreds of services, then you were grossly misled.

⬐ yogthos

I linked a talk from Walmart that explains exactly how they're using Clojure. I don't think I'm misrepresenting anything here.

⬐ darksaints

You absolutely are. You name dropped Amazon as some sort of proof that Amazon is used at scale, completely misrepresenting the scope of usage. Simply put, Clojure at Amazon is an insignificant and inconsequential symptom of a massive service oriented architecture with tens of thousands of software developers across four continents making independent decisions on how to write their tiny services.

⬐ yogthos

I think anything that's part of the sales chain can't be dismissed as insignificant. Just because Amazon uses other technologies, that doesn't diminish its importance.

⬐ jb1991

I can appreciate your desire to share the good news about Clojure adoption, but I don't think the language is in need of defense. It's used a lot all over the place, and you shouldn't feel the need to convince others of that. Because even if it weren't used hardly anywhere, it would still be a great tool for those of us who do use it. That it is in fact in use in a lot of places, regardless of its specific role, is just a nice added bonus.

If someone doesn't want to use it for this reason or that, it's their loss not ours. Those who need to find Clojure eventually will, because there is nothing else like it.

Aerospace is not performance critical, at least not the overall industry. There are parts that are important, but a lot of them are not. I watched a talk where a company used clojure for diagnostics (board metrics and faults (https://www.youtube.com/watch?v=iUC7noGU1mQ) for maintanenance).

⬐ gaius

Everyone's playing the flops/W and flops/U game tho'

Clojure at Boeing[0]

[0] https://www.youtube.com/watch?v=iUC7noGU1mQ

⬐ _halgari

Can you link a quote or a point in that video? What does Boeing's use of Clojure have to do with Cognitect?

⬐ silentmars

21:40. He mentions in the video that they had a one-producer, one-consumer input queue that they originally implemented with clojure.lang.PersistentQueue. They engaged Cognitect for some code review/consulting, and Cognitect's advice was to use a regular Java ConcurrentLinkedQueue for this instead.

I think this particular example supports this "Cognitect snake oil" theory very poorly. I don't think PersistentQueue can be properly considered a first-class data structure in Clojure, as it doesn't even have a constructor function in clojure.core. The Clojure documentation, and the other writings of Rich Hickey and Cognitect don't encourage people to use this data structure. It exists, I think, for completeness and because there are some situations where it's appropriate, but unlike the core Clojure persistent data structures - maps, vectors, seqs, etc. - it's not designed as a general abstraction that covers the vast majority of general use cases.

Clojure is meant to be a practical language. It's hosted on the JVM and other platforms, and designed to make it is easy to use what those platforms provide. Where it's sensible to do so, Cognitect and other Clojure developers would certainly advocate using Java libraries to solve problems.

The other thing mentioned in the GP post was the idea of not using STM. This falls under the same umbrella. There are problems for which STM is the best solution, but there's a big space where something simpler is the right answer. In my observation, overuse of Clojure's STM is far more often the result of a developer impulse of "wow this is a cool looking feature, I want to try it" than any advocacy by Rich or Cognitect.

I also have some firsthand knowledge here, having been involved in a Cognitect engagement. I have some concerns about Cognitect as a result, but certainly nothing like this suggestion that Clojure is a real manifestation of the old fake Bjarne Stroustrup interview. [1]

[1] https://www-users.cs.york.ac.uk/susan/joke/cpp.htm

⬐ agounaris

One of the things that is impressive, is the amount of "real life" applications clojure is apparently capable of, compared to other relatively new programming languages. I always was expecting that avionics software would be created using low level languages or something like ADA for example. Really interesting talk that opens a very wide area for clojure!

⬐ clem

Bear in mind that avionics software as a whole is a broad category that includes everything from fly-by-wire flight controls to the onboard entertainment system. Each system is classified under an appropriate Software Level as specified in DO-178C:

https://en.wikipedia.org/wiki/DO-178C#Software_level

The OMF system described in the video is Level E, meaning it's failure would have no safety impact on the aircraft. This gives us greater latitude in choice of software solutions. The higher levels, however, have strict requirements regarding latency and memory management that would automatically preclude the use of Clojure or any language with garbage collection.

So, as always, it's selecting the right tool for the job.

⬐ agounaris

Cheers, interesting info

⬐ paulydavis

From my experience most of the work I have done in the last 5 years is in C for Level A - C (and D but that is changing). Ada is only used on legacy projects that started out that way. We have one level D project that uses embedded Linux and a technicolor assortment of languages. E projects generally are a free for all with what is used.

⬐ pron

SCADE is also used in levels A-C:

> At present, more than 98 system types have been certified using SCADE DO-178B/C certified tools, for more than 53 aircraft programs, by multiple certification authorities, worldwide, such as the FAA, EASA, Transport Canada, and ANAC, for Levels C to A.

http://www.esterel-technologies.com/industries/do-178b-and-d...

⬐ paulydavis

Yeah Simulink produces C code too. Doesn't SCADE produce c and Ada code to be compiled for the target? I mean most Control laws (application code) is now modeled and produces C code. I would not even call SCADE and Simulink a language. Custom OS's that run that SCADE code is written in C.

⬐ pron

Right, SCADE compiles down to C, but the development and verification are done in SCADE.

⬐ clem

I'm one of the leads who worked with Donevan on this project. Feel free to ask me any questions and I'll answer as best I can.

⬐ agounaris

I'm interested in the underlying platform and how the software is being shipped? Do you need to go through a specific process in order to install a new version or a bug fix?

⬐ clem

Anything in a regulated industry such as aerospace tends towards the process heavy. Our requirements get tracked in our QMS system that ensures we're AS9100-compliant. There's a final test-for-credit step after which the software part should be considered hermetically sealed. Any software change requires a new test-for-credit round that likely takes an extensive amount of time.

So, in short, developing for aerospace is not agile. :-) It's the Niagara Falls of waterfall methods.

⬐ paulydavis

I work at BAE and we do quite a bit of software for Boeing. DO178 C could allow you to do Agile if the PSAC was set up from the beginning for that. The problem would be the cost points and contracts and customer buy in that would be needed on all sides. But alas for now it is the mother of all Waterfall methods.

⬐ dolbydc

We developed OMF using agile scrum, not waterfall, but we ultimately were running our agile process within a waterfall

⬐ hcrisp

It's not widely known but Python supports a certain amount of functional-programming idioms. It also supports event-driven data flow. Was it considered at the beginning of the project? (was it even one of the languages Boeing supports?) Why would or why would it not be a good choice for this health monitoring application?

⬐ yogthos

The big difference between Python and modern functional languages is that Python defaults to mutability. Clojure is immutable by default, and that makes it much easier to reason about code in isolation. When you're working on a large project, it's really valuable to be able to make a change in one place and know that you're not affecting something in another.

When things are passed around by reference, it becomes very difficult to guarantee the scope of any change. Even when using immutable data structure libraries in a mutable by default language doesn't really give you many guarantees. As soon as somebody puts a mutable object into your immutable data structure all bets are off. So, you really want a language that defaults to immutability and has different semantics for working with mutable data.

⬐ dantiberian

On the video it sounded like it was 16,000 lines of code. Was that the amount or did I mishear it? That was claimed as one of the largest Clojure codebases, which seems unlikely.

⬐ clem

That's correct. As for size relative to other projects, we came to that conclusion by combing large GitHub clojure projects and comparing non-blank lines. For instance, LightTable comes in at around 12,000 lines. Clojure is a darn terse language.

Of course, there may be private repositories which are larger (thus the weasel words "one of"). Corrections welcome. :-)

⬐ dantiberian

From memory, CircleCI have around 100k LOC. Nonetheless, it's very cool getting Clojure on a plane.

⬐ clem

Thanks. Found a reference to the CircleCI code base:

http://www.ccs.neu.edu/home/samth/typed-clojure-draft.pdf

I wonder how their move away from clojure.typed has impacted code size.

⬐ dolbydc

I was made aware of a private Clojure project that is comprised of over 30k lines. So we aren't the largest, but probably the first to be on a commercial aircraft.

But as Tim pointed out auditing of open source projects had most far smaller than 16k. Lamina a very feature rich library I think was on the order of 6k.

Perhaps I should have gone with "Clojure on planes" as my title.

⬐ clem

Or "States On A Plane" with a photo of Samuel L. Jackson. :-)

⬐ dolbydc

I re-ran SLOC using the sloccount-clojure tool, we sit at about 34k lines using that tool. Instead of my jenky find/egrep/wc.

⬐ aaron-santos

I'd consider 16,000 on the small side. For comparison, I've been working on a Clojure roguelike as a hobby project and it's in the ~18,000 LOC range.

⬐ dolbydc

Aaron, how are you counting the SLOC? I am not doing a simple `wc -l` on all clj files in our project. I am looking for lines that include either closing parenthesis or closing brackets. It isn't exact. A better count would be to count the # of forms.

I get 17k in your project with find . -name ".clj" | xargs wc -l but 8k if I run 'find . -name ".clj" | xargs egrep "[)\]]" 2> /dev/null | wc -l'.

If I just run `wc -l` on our project I get 35k lines.

8k SLOC is still a pretty impressive size project considering the audit of several open source projects that I did were mostly below 8k SLOC.

⬐ lemming

BTW this is the largest Clojure project I've heard about: https://twitter.com/hlship/status/631935954039652352. That's a pure Clojure project.

⬐ aaron-santos

I used sloccount-clojure to count lines, but before running it I made one change so that it would include .cljc files.

Then I summed both robinson and zaffre (0.4.0 branch) seeing as they both used to be part of the same project and have only recently been separated.

⬐ lemming

I develop Cursive - it's closed source, but it's around 31k LOC Clojure, 23k Java and 5k Kotlin, all as counted by cloc. I'm not sure what's up with your find command, but that reports 5k LOC in Cursive, it's definitely more than that. Straight wc -l reports 74k.

I'm pretty sure my code has more bugs than yours, though :-)

Anyway, very interesting presentation, thanks - it's great to see a project like this in a space I wouldn't have expected it. I'm very surprised (and pleased) to know that Clojure is on Boeing's approved language list - I'd love to know how that came about.

⬐ 147

That's what I heard in person

⬐ namelezz

You are right. It's not the largest Clojure codebase(Language Breakdown of Storm [1]). There may be reasons why they think their Clojure codebase is largest.

[1] https://www.openhub.net/p/apache-storm/analyses/latest/langu...

⬐ neurotech1

Does Boeing have a policy on using and defining acronyms?

Interesting presentation, although I noticed Donevan used a few acronyms that some people may not be familiar with.

⬐ dolbydc

Not sure if there is a policy. Are there acronyms in particular, I tried to limit it to the couple applications we interface with. Which truth be told I don't know off the top of my head what they stand for. More importantly is what the application does. I worked at Boeing for 6 years and people talk in acronyms most the time not knowing what it stands for, just what the system does.

⬐ namelezz

Why Clojure and not Scala?

⬐ mateuszf

I'd pick Clojure between the two because simplicity.

⬐ noir_lord

In the video he mentions that libraries went EOL during development, given the the predicted lifespans of modern airliners how do you plan on been able to build the software a decade from now?

⬐ dolbydc

If needed we or Boeing would take over the lamina library, or migrate to an alternative like core.async or manifold.

⬐ aaimnr

Isn't it amazing that they built a real-time diagnostic system for Boeing plane in Clojure with a team that haven't previously used Clojure? They basically were learning on the fly, coming from OO background, about map/reduce, immutability etc. Kudos for being really open when choosing the best tool for the job after initial research (among the reasons behind picking Clojure the guy lists functional reactive style and being able to easily parse DSLs). Code brevity was one of the positive side effects, which made code reviews much quicker. Impressive

⬐ iagooar

> They basically were learning on the fly

I chuckled on this. Pun intended? :)

⬐ jakub_h

I'm getting kind of sleepy here at 2 AM and my brain misarranged the headline words into something like "Development of an application in Clojure onboard the Boeing 737 Max". So it seems like an easy mistake to make!