unboxed_type

13 ms·

1. 61.▲
   by unboxed_type 10y ago

   Good point. As far as I know there are no DO-178B complient C++ libraries available yet (STL, for example). If you know any please point out. My reasoning is as follows: While civil avionics must comply with regulatory safety standards, m
2. 62.▲
   by unboxed_type 10y ago

   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
3. 63.▲
   by unboxed_type 10y ago

   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% te
4. 64.▲
   by unboxed_type 10y ago

   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?
5. 65.▲
   by unboxed_type 10y ago

   Here is my 50 cent. Zephyr OS from Linux foundation: https://www.zephyrproject.org/
6. 66.▲
   by unboxed_type 10y ago

   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 langu
7. 67.▲
   by unboxed_type 10y ago

   One must not compare dynamic type language ergonomics with a static one - different niches ;-)
8. 68.▲
   by unboxed_type 10y ago

   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. A
9. 69.▲
   by unboxed_type 10y ago

   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) ?
10. 70.▲
    by unboxed_type 10y ago

    Thanks for that clarification! It is a great pleasure to talk with an knowledgeable person like you.
11. 71.▲
    by unboxed_type 10y ago

    For those who are interested in an underpinnings of KSI: https://eprint.iacr.org/2014/321.pdf
12. 72.▲
    by unboxed_type 10y ago

    Thanks alot for sharing this!
13. 73.▲
    by unboxed_type 10y ago

    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 ;)
14. 74.▲
    by unboxed_type 10y ago

    Why is it so important what language it is written in? :-)
15. 75.▲
    by unboxed_type 10y ago

    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.
16. 76.▲
    by unboxed_type 10y ago

    Please note that you will be asked to solve rather difficult codility test for rather short amount of time.
17. 77.▲
    by unboxed_type 11y ago

    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 -)
18. 78.▲
    by unboxed_type 11y ago

    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 loo
19. 79.▲
    by unboxed_type 11y ago

    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
20. 80.▲
    by unboxed_type 11y ago

    Why this paper deserves attention in your opinion? I found nothing remarkable there.
21. 81.▲
    by unboxed_type 11y ago

    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
22. 82.▲
    by unboxed_type 11y ago

    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.
23. 83.▲
    by unboxed_type 11y ago

    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
24. 84.▲
    by unboxed_type 11y ago

    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.
25. 85.▲
    by unboxed_type 11y ago

    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 m
26. 86.▲
    by unboxed_type 11y ago

    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