Julia with respect to reliability, sustainability, critical application, dynamic/static typing, big data, HPC?

No, and hopefully no one in their right mind is even thinking about this.

Imagine a spectrum where you trade off convenience and flexibility for catching errors at compile time. On this spectrum, Julia and Ada are very far away, and you will find languages like C++, C, and Fortran in between (and of course, more exotic ones too).

Julia was explicitly designed to be dynamic, convenient, and fast, with the compiler there to help you by making your code run fast if you cooperate with it, but rarely enforcing anything at compile time. In fact, apart from trivial syntactic mistakes, the effort of “getting your program to compile” is mostly unknown to Julia users.

3 Likes

Who said anything about making a trade-off? I wasn’t proposing to take anything away.

Also, I was talking about “agda” with an extra g, which is not the same as ada. It uses proof by reflection, which Julia might be able to do if it had some extra inductive type features.

The new features don’t have to exactly resemble a previous language, just learn from it.

Are inductive types threatening to other aspects of the Julia language that would cause trade-off?

Not in the part I quoted.

Hard to say without a concrete proposal. But it is also unclear what their benefit would be.

My understanding is that in Julia, types are mostly used for dispatch, and by the compiler, but not for enforcing anything. In fact, Julia relishes the fact that not all expressions have a type at “compile time”.

A new keyword like inductive type could be used to generalize Julia from only type dispatch to make julia able of more general proofs.

1 Like

IMO, a number of things, among them that Ada has been used in this domain for a while, and now has SPARK.

I don’t think Julia is well suited for this domain, nor do I think it would be worth the effort to try to make it so. Julia already has a nice focus, scientific computing, and fairly broad scope outside of that focus. If the developers were looking for more challenges, then embedded systems would be my suggestion, since one would like to deploy trained machine learning models there and I suspect (but have not done the experiment) that Julia is currently not suited for tiny embedded systems. Of course, I’d love to be wrong about that.

3 Likes

The only reason I mention it is purely due to my interest in the mathematics of it, I recommend looking at the referenced paper Engineering Proof by Reflection in Agda

Abstract. This paper explores the recent addition to Agda enabling reflection, in the style of Lisp and Template Haskell. It gives a brief introduction to using reflection, and details the complexities encountered when automating certain proofs with proof by reflection. It presents a library that can be used for automatically quoting a class of concrete Agda terms to a non-dependent, user-defined inductive data type, alleviating some of the burden a programmer faces when using reflection in a practical setting.

what does @jeff.bezanson have to say about it with respect to Julia?

Has any “real world” safety critical system been developed using Haskell, Agda, Idris, or the like?

I suspect there’s a bit of a mismatch between what academic PL theorists like to work on and what is actually needed and desired. If this were not the case, there probably would have been no need for Julia, since Haskell was already there, and has some scientific computing libraries.

Right, there has been some long standing discussion about adding some kind of explicit interface mechanism to Julia. @StefanKarpinski briefly describes the expected behavior of the feature, if it should ever make it into Julia

I’m all on board with that description!

1 Like

When I think about it, I am not sure this is something that is either feasible or desirable.

Many of the implicit interfaces in Base are currently not even documented, or even generally recognized as interfaces despite the fact that people treat them as such. Very few package authors document interfaces, which suggests that doing so is burdensome. So what we have is “duck interfacing”, gradually becoming documented on demand (but not formally described and verified using a DSL) and I have come to recognize this as a fine solution to a difficult trade-off.

(And this topic is turning into a somewhat off-topic discussion. But as the original question was very hazy and the OP did not show up again, I think this is fine too).

2 Likes

Should we move this to another thread? I’ll let someone else decide.

I suspect that if there were a way to document interfaces in the Julia language then we’d see more documented interfaces. The evidence I have for that assertion is very roughly provided by Python and Javascript/Typescript, where we see a subset (certainly not yet the majority!) of those communities opting in to providing explicit annotations.

I would prefer to have this in the language, so that tooling to provide more checking would naturally arise, and perhaps even some social pressure to write explicit interfaces would come about too if there were a language provided approach.

Some interfaces are already documented, there is nothing preventing anyone from following this practice.

I suspect that the real reason for the absence of many more examples is that good interfaces are rather difficult to design, and evolve organically. At some point people realize that what they implemented can be abstracted as an interface; the threshold is rather fuzzy.

3 Likes

I was unclear. When I said “document interfaces in the Julia language”, I meant having some actual annotation, like the aforementioned interfaces, in the Julia language itself, as was mentioned in the Julia issue I linked to. Any language of course allows external documentation, but that’s as helpful as comments. A language feature would facilitate external tooling, and at least according to the issue mentioned, would not hinder your preferred method of external documentation.

I think it’s worth considering that designers of other dynamically typed languages find the use of types to be useful in very large code bases.

It is not clear to me what the tooling would be in this case.

A static type checker like mypy/pyright/pyre would be great. But I know that “type checking” is actually listed in Compiler work priorities so I suppose the core team is thinking about this as well.

Sorry, I don’t understand how this came up in this context. AFAICT that article is talking about declaring types for variables, eg

In statically typed languages, developers typically specify the type of a variable or a function parameter when they’re declared, for example, using the keyword int to specify an integer, or str to specify a string of characters, to use two simple examples.

Julia already has this: when you specify types for a method, they are effectively checked, and for all other values you have type assertions.

I am not super-familiar with Python and Typescript, but I would suspect that Julia’s problems are somewhat different. With its rich parametric type system, the main problem is not verifying/asserting the type of something (that is trivial), but figuring out what that type should be.

This is a hard problem, and it is not even clear that exposing/specifying this information should be part of an API. Eg if I do

julia> StaticArrays.SVector(1,2,3)
3-element SArray{Tuple{3},Int64,1,3} with indices SOneTo(3):
 1
 2
 3

should the user care about all the type parameters of the result, or are they just implementation details the maintainers of StaticArrays can change at any time? I am inclined towards the latter.

the user should not care, but the developer of packages using StaticArrays needs to know the parameters and if they change later on, this is what semantic versioning is for

I disagree — I would propose that even the packages that use a package should not care about the fine details of its concrete types per se, unless they are part of the API, but then it is probably not the right API.

Abstract types are a different matter. But in most cases those are best left as an internal detail, too, and the relevant functionality should be exposed via traits. My 2¢.

Well, in Grassmann.jl I actually need to use the implementation specific parameters of StaticArrays, otherwise I would not be able to write the @computed struct for the MultiVector type. So, in reality, the details do make a difference, and a change in the parameters would require compatibility changes. In this case, there was no way around it.

Hello Tamas (and others contributors),

Sorry to answer just now but I was really busy these last weeks. Nevertheless, I follow more carefully this blog now, don’t worry.

Thanks very much for your contributions and for the contributions of the others ! :slight_smile: Many informations … thanks … .

Tamas, I agree, my initial question is large and could be split.

Nevertheless, I am indeed interested in different questions concerning Julia and in having different opinions. These questions includes :

  • reliability for critical apps with minimum response time and high availibility,
  • reliability for long-life process (memory recycling management ?),
  • reliability with intensive processing computation and capacity to manage big amount of data (which explains my question about K. Bouman) compared to classical langages in app. math. (eg Fortran/C/C++),
  • reliability of bug free developpement regarding the use of a dynamic type langage compared to a static type langage.

At least, are there benchmark tests for the 3 first points ?

Thanks again to all contributors ! :slight_smile:

I wondered were the words come from: fiabilité (fr) is reliability, pérennité(fr) is sustainability.