sfrank

So, like Delaware?

Like iterate (https://common-lisp.net/project/iterate/)

For automotive software the ISO 26262 is the equivalent to RTCA DO-178 in avionics. ISO 26262 highly recommends that ASIL C and D-classified systems utilize semiformal and formal verification among other techniques to verify software unit design and implementation.

That is because the formal method supplement of the DO-178C is RTCA DO-333. There you have about a hundred pages concerned with the application of formal methods.

And what the OPAL functional language [1] did since the mid 80s. Though the concept there is expanded from simple reference counting by additional static analysis during compile time (making use of the functional semantics of the language) to avoid reference counting when for example the compiler can find/prove sequential increment/decrement counts, then the reference counting code is eliminated.

[1] https://github.com/TU-Berlin/opal

No, a domain-consistent all-different propagator such as the one desccribed in [1] is sufficient to determine a valuation domain for a Sudoku puzzle without any search.

Of course that does not hold in general, but in the special case of Sudokus and problem modelling by a domain-consistent all-different propagator, no search is required for a solution.

[1] A filtering algorithm for constraints of difference in CSPs, J-C. Régin, 1994

Yes, but even better there is the global constraint geost [1] which is specifically for this purpose in k-dimensions; see also [2] for a more detailed presentation.

Unfortunately, Gecode does not provide it (and you would have to express it in form of other, more lower level constraints which gets quickly complicated), and neither does Google's OR-tools which have a nice Python interface.

There is JaCoP which provides the geost global constraint and makes it available via the declarative MiniZinc problem description language so one needs not to use the Java API.

[1] http://sofdem.github.io/gccat/gccat/Cgeost.html [2] https://www.sics.se/~matsc/docent20090209.pdf [3] http://jacop.osolpro.com/

The DO-178B/C explicitly does not specify how verification is done but describes the properties that are expected of the verification evidences that you submit to the certification authorities; so formal verification is perfectly fine as one item on your verification check list. In particular DO-333 amends DO-178C with specific topics concerning formal methods.

For example Astree [1] has been developed for decades now, with Airbus as one of the major sponsors.

[1] http://www.astree.ens.fr/

Sure you can do however, since Ruby allows destructive updates, why not use one of the established/traditional imperative data structures and then apply techniques to make them "persistent" (i.e. immutable in the functional programming sense as is also used by Okasaki and of course not using the trivial technique of copying the whole thing). Such techniques are e.g. presented in CLRS if I remember correctly.

It is not that Okasaki was the first one to implement any functional data structure. People have been doing this before and also in purely functional languages such as Haskell, ML, or Opal). He was the first to give a very nice overview, showed some new designs and even more important, showed a way for time complexity analysis (in a lazy evaluation context).

And it is this last part of the thesis that many people overlook: the importance of lazy evaluation (and thus the implied fundamental optimizations/evaluations performed by the compiler/runtime) for most of the presented data structures (i.e. everything with an amortized time complexity). Simply implementing Queues as presented in the thesis and not having a lazy language will lead to a very different time complexity than is proven there, because lazy semantics is vital for the given complexity analysis.

This is also the reason, why e.g. Clojure (or Opal from the early 90s, [1]) use other data structures to ensure functional (i.e. persistent) semantics in an eager/strict evaluation model.

[1] 1994, http://projects.uebb.tu-berlin.de/opal/trac/raw-attachment/w...

Well, not my area, but a little googling brought up this: http://www.inf.ethz.ch/personal/cellier/MS/andres_ms.pdf (well, there goes my evening). I don't know, but I find the decomposition quite intuitive.

Well, since both are implementations of the Modelica standard I would guess they are pretty much the same, though I do not know MapleSim or your problems with it.

This is simply a different view to model systems such as can be done in Simulink. Simulink has a (differential) equation-centric view whereas Modelica (of which SystemModeller is an implementation using the mathematical capabilities of Mathematica) has more an object-oriented view where external interfaces are exposed and connected and the behaviour as expressed by the differential equations is hidden. Modelica is a standardized language, see e.g. http://openmodelica.org for an open source implementation.

It is simply not true that there wasn't a Simulink alternative until now. Modelica exists since 1997 (cf. http://en.wikipedia.org/wiki/Modelica) and there are several commercial implementations of it: Dymola, MapleSim, MathModelica (which now in v3 has been purchased by Wolfram and has been rebranded as SystemModeller), CATIA Sytems and probably some more.

Adaption of Modelica has been slow since engineers are more exposed to Matlab/Simulink during their education and this base is slow to change. Considering license, training and experience costs this is certainly understandable. However, I know that several German car makers are gradually changing over to Modelica since the models are easier to understand for new people joining the projects (and to escape the vendor lock-in of Simulink).