unboxed_type

Well the article says that F-35 runs operating system compliant with DO-178B, right. But it does not say that control logic software (applied software) was a subject to DO-178B certifcation. Anyone can buy a license for DO-178B RTOS, it is not very expensive actually. But to certify your own control avionics algorithms is a whole different story. Agree?

As far as I understand all vehicles you mentioned are not subject to DO-178 regulation. If they were then C++ code would have been much less likely be used. It is because C++ code is much more difficult to prove correct either using 100% test case coverege (DO-178B) or thru formal methods (DO-178C). Please correct me if I am wrong, I am doing a research on a similar topic.

Is it legal to use such robots in human-populated environments like office building or factory? What if it causes harm to somebody? Any thoughts?

Here is my 50 cent. Zephyr OS from Linux foundation: https://www.zephyrproject.org/

Wow! Ok. Well yes, as far as I know both Joe and Rob agree on that it is accident that Erlang have implemented 'actor model' thing. Also its interesting to note that functional nature of Erlang is very different to ML-family languages. Authors used all these functional stuff because of pragmatics in the first place and not because of solid theory underpinnings.

One must not compare dynamic type language ergonomics with a static one - different niches ;-)

Its interesting how you squeezed 'Erlang language' into some syntax choices. Erlang is about actor model, not about pattern matching. Joe had his inspiration from Prolog - it is a well-known fact from publicly available sources.

Anyway, thanks for the article, it sparked some emotions in my brains :-)

Hello! What are the reasons one would want to write C code in Haskell DSL instead of supplying ones C code with annotations and proving those annotations semi-automatically instead (Frama-C) ?

Thanks for that clarification! It is a great pleasure to talk with an knowledgeable person like you.

For those who are interested in an underpinnings of KSI: https://eprint.iacr.org/2014/321.pdf

Thanks alot for sharing this!

It is important, because you will not find any Go-developers on the market, so if you are serious about using it then think twice ;)

Why is it so important what language it is written in? :-)

You could check design flaws using model checking and/or rigor formal verification process. I think it is what they meant under 'advanced mathematics' term.

Please note that you will be asked to solve rather difficult codility test for rather short amount of time.

It is interesting from performance and low resource consumption point of view. Great work! I wonder if someone would like to do the same in assembly language for even more crazy experiment -)

I would like to mention that Coq is also used to extract _verified implementations_ rather than model checking abstract algorithm design (as in TLA+). This property might be very desirable depending on situation. As for me this property looks very appealing.

Also take a look at this thread, were I briefly describe our experience of using all the spectre of verification tools. https://news.ycombinator.com/item?id=10220264

Why this paper deserves attention in your opinion? I found nothing remarkable there.

If under 'bitrot' you assume random bit flip here is the quote from that paper: << Project Zap [53,60] and Rely [8] explore using type sys- tems to mitigate transient faults (e.g., due to charged particles randomly flipping bits in a CPU) in cases when the system keeps executing after a fault occurs. These models consider possible faults at each step of a computation. The type system enables the programmer to reason about the results of running the program in the presence of faults, or to ensure that a program will correctly repeat its computation enough times to detect or mask faults. >>

There is a gap between human understanding and reality, so any abstraction including mathematics may have a flaw, in my opinion. But refinement of that understanding is crucial to get better at building mostly-reliable systems.

In short: Spin and TLA+ are "push-button" mechanisms where computer are trying every possible trace of your system to check system state against supplied invariant. Pros: You don't have to think much about your systems thin properties before verifying. Cons: State space explosion so not every real system is a subject to such verification.

Coq,Agda: Manual/Semi-manual correctness proof of your system. You can reason about even "infinite" systems with this approach using relatively little computation resources. But to do so you have to gain a _deep_ insight about your system behaviour, computation semantics, network semantics (if distributed system is checked) and other properties. If you are lucky you can proof property under question, even it assumes very large moving parts. If not then you cant tell that this property can be proved at all. So these are more like platforms for quasi-manual deduction.

F* is trying to take up a niche between manual proof and quasi-automatic proof using SMT solver for those of theorems which can be proved this way. The problem is that SMT solvers are generally suck, there is no sound theory behind it, so it is more like guessing in my opinion.

Thanks for the link. I read about TLAPS. It seems it relies on SMT solver to uncharge proof obligations, and no way for you to manually prove your claim using lower level tactics, like in Coq. So you rely on heuristic nature of SMT solver.

About Spin[1]. If you compare the user base of Spin with the user base of TLA+ I bet you will wonder how many users out there were using verification tools all those years. Lamport released his tool like 20 years later than SPIN started to spread. He did a great job, but there is no innovation in my opinion.

I think that serious industry players like Intel, Google or NASA are using all spectre of verification tools, including self written tools. Intel is using there own tool for some of their chip verification AFAIK. My colleague went into Intel to help develop verification scripts using this tool.

TLA+ has been promoted by Amazon with their latest technical report. Yes, it has more expressive types (records,tuples,sets), but it comes with a cost of lowering your verification performance rate. There are many subtle tradeoffs to make.

We tried to use several formal verification tools in our latest distributed project. We tried Spin, TLA+, mCRL2, Coq. There is its own philosophy, pros and cons behind each tool, but in our case Spin made the best job: we had to invest not so much time but found many concurrency bugs in our distributed algorithm. Its pros is that it has very basic data types and not very good parallelism support nor in multi thread nor in multi-node form.

[1] http://spinroot.com/spin/whatispin.html

Pros: PlusCal is relatively easy to use and understand. TLA Toolbox is self contained. You have an editor, a model checker and other tools right out of the box. Two or three books written by Lamport. Nice material base. Theory behind this model checker is relatively lightweight. Compare it with some sophisticated process algebra, for example.

Cons: PlusCal is not able to handle process spawn operation, as far as I know. So if you are to model real system where clients come and go, you have to write your spec in pure TLA+ which is unmaintainable, because it is just a logical assembler.

State explosion problem.

Java as implementation language. So you are using your CPU cycles not the best way.

Built-in proof system is not able to and was not supposed to check your proof. To do this you have to use some other tools like Coq (fix me if I am wrong)

Nearest competitors in that nich: Spin (yeah!), Alloy, EventB. Just let you know that there are alot of model checkers out there.

My personal impression is that the language infrastructure is not mature enough. As of version 2.0 you cant install Elm on Linux platform from npm because of broken repo link or something (it is known bug but looks like no one cares to fix it). But even you managed to install it, Elm itself does not work behind corporate firewall because it rely on Haskell HTTP library which suck (they fixed this bug in the library but please wait for another Elm release for this to work).

The language looks very interesting and promising, I am very pissed by the fact that I had no chance to try it in our latest project because of those miserable bugs.