[pjmlp]

I guess the French and US military using Aonix real time JVMs for weapons control and monitoring are the right set of persons to answer your question.

Also some military think memory leaks are irrelevant on missiles, given the ultimate garbage collector.

[touisteur]

Well it all depends how 'hard' your real-time is. If you go with Atego/aonix, you can get down to almost-C-Ada-like latencies but be ready to change your java coding style. Sliced-time GC works OK until you put too much pressure on it (concatenating logging strings that you're not going to record or display... allocating tons of small objets for local uses... Programming in 'Classic' java...) and it can't clean up fast enough... In the end you code in a small and sad watered down subset of java... I mean : java is everything (almost, except for primitive types) on the heap ! Avoid java collections (use javolution or hppc-rt instead), avoid auto-boxing, no local allocation, no String concatenation, no Selector API ('select' in java nio...) because it allocates like mad... God help you if you need to stream some amount of data via TCP. And be prepared to spend some time to fine tune the GC. You also take a hit on performance and compilation time compared to hotspot (you need aot compilation for real-time, the java runtime seems not as optimised... Not as many man-decades of work on it).

All in all I'd rank it 'easier' than C in developer comfort and proficiency but frankly, if you don't do C, I'd just go directly to Ada...

[pjmlp]

Thanks for telling your Aonix experience.

I would just argue that un these domains 'Classical C' isn't used, given the constraints regarding language features, using stuff like MISRA-C and similar.

Fully agree with Ada comment, even better if using SPARK.

In any case, many military seem more focused on being easy to hire recruits that already know how to program than training them, hence the ramping up of Java adoption.

[touisteur]

Well the argument seems to be that it's easier to hire 'experienced' java developers (hear: have 'java' on their resume...). But the people you get are for the most part either inexperienced (fresh out of school) or you have to break all their classic-java muscle memory. Not sure about the tradeoff here, when you compare training in Ada/SPARK.

You're right about Misra C. Even with Ada you'll end up banning dynamic memory allocation and some stack-exploding stuff, but you still have alternatives like storage pools ('looks-like-dynamic' memory allocation) and Controlled types, and at least you get a stack for structured data types and not just for primitive types...

[bigiain]

Heh - saw that on Twitter last week: https://twitter.com/pomeranian99/status/858856994438094848

"Memory leaks on missiles don't matter, so long as the missile explodes before too much leaks."

[nickpsecurity]

It's called real-time, garbage collection. It occurs predictably on regular intervals before enough leaks happen to blow missiles up or whatever other tragedy. Aonix and some other vendors have had it for a long time now. Meanwhile, mainstream found out in the past, few years that Go could achieve "low-latency" garbage collection. The field can do more than many of them think given the countless person-years invested in so much GC research and product development. I can't even track all of the GC's especially once they started using genetic algorithms and such to automatically make them.

EDIT to add: It says "Ada" and "Rational." That's an Ada forum. That language has little protection for temporal safety in the 1990's. More than many but not at Rust level or full leak prevention.

[touisteur]

Seems AdaCore is working to add some form of borrow-checker to Spark :-) https://cps-vo.org/node/34575

[nickpsecurity]

In case you're interested, here was a reply from Yannick at AdaCore:

https://groups.google.com/d/msg/comp.lang.ada/H35QcYiWR1Y/jJ...

It seems they're adding a little bit of it for SPARK but not critical, dynamic part. I asked him at the end if they plan to go full, dynamic safety for full Ada if the SPARK experiment succeeds. Awaiting the reply.

[touisteur]

Hey thanks for the pointer to this thread. Allowing pointers in SPARK would be incredible... Today SPARK is so interesting because it's not all-or-nothing. So some parts can be SPARK (with different levels of proof), others Ada, etc.

One of the main limitations of the tech is 'no pointers' in SPARK mode. There are some tricks to hide pointers (you may want to look up the SPARK deployment guide : http://www.adacore.com/knowledge/technical-papers/implementa... ) but it would allow so much more code to be SPARK-compatible. Even in the embedded space sometimes you need pointers and linked-lists and hashmaps (and the new formal containers don't do it for you)... Frama-C allows (and seems to work with) pointers, I don't know how Well.

For Ada you can already go a long way (memory safety and data races) with protected object (nice semantics, check performance), not null pointers, controlled-types... But we're far from Rust's borrow-checker and move semantics. The name Unchecked_Deallocation (to instantiate 'Free') says it all.

Can't wait to see some progress on this !

[nickpsecurity]

I don't see anything about safety for dynamic, memory management in that link. It just talks about correctness. I'm specifically wanting affine types and ownership system that let SPARK go from static to dynamic.

I do like them splitting it into several levels, though. That worked under Orange Book for security.

[touisteur]

My bad, slides are not available yet... There's a mention in there about some rust-like ownership proof mechanism in their roadmap. I thought about our last exchange on SPARK & rust when I saw this :-).

[pjmlp]

AdaCore hired the guy that designed ParaSail, however the language development is a bit slow.

https://forge.open-do.org/plugins/moinmoin/parasail/FrontPag...

[nickpsecurity]

In case you're interested in details on this development:

https://news.ycombinator.com/item?id=14346032