Top all-time · #728
spinroot.com
Personal blog · spinroot.comprogrammingsystems
spinroot.com is a personal blog at spinroot.com about programming and systems. Since 2008, 89 different Hacker News readers have linked it 114 times, most often “The Power of Ten – Rules for Developing Safety Critical Code”. No feed was found, so read it on the site itself.
Rarely recommended · 5 of 40 sampled comments recommend it?
Why HN links it
HN readers link spinroot.com, Gerard Holzmann's site, mainly for the Power of 10 rules for safety-critical C code, plus the SPIN model checker and Pico pages.
- Recommended for · 5 comments
- Praised as easy to understand and verifiable, with rationales explained; one commenter calls a Pico page interesting.
Summarised by Claude from a sample of 40 HN comments that link here. Each comment is marked recommending, critical or neutral (citing without judging); how this works.
Most-linked posts?
- The Power of Ten – Rules for Developing Safety Critical Code18 people · 18 mentions · first linked 2013-10-22
- Verifying Multi-threaded Software with Spin14 people · 19 mentions · first linked 2008-03-14
- The Power of Ten – Rules for Developing Safety Critical Code [pdf]11 people · 12 mentions · first linked 2022-07-05
- Rules for Writing Safety Critical Code (2006)7 people · 7 mentions · first linked 2012-12-06
- PJW's Face7 people · 7 mentions · first linked 2011-12-19
- PJW's Face(2018)6 people · 6 mentions · first linked 2022-06-04
- /3 people · 3 mentions · first linked 2020-01-17
- Code Inflation (2015) [pdf]3 people · 3 mentions · first linked 2016-08-14
- /2 people · 2 mentions · first linked 2018-07-09
- Bell Labs, building 2, 5th floor: main occupants for each office over the years.2 people · 2 mentions · first linked 2010-02-12
What Hacker News says?
> Does it make application programming easier, less error prone, more accessible? If you want to write systems that improve the safety of application programming, it helps to have a lower-level understanding of what is happening. As for Mars, if articles like this ( http://spinroot.com/dcas/ ) are any indication, there will need to be a lot of systems programming and especially tool building that requires deep syste…
Comment linking /dcas/
on “Announcing Starfighter”Submitted The Power of Ten – Rules for Developing Safety Critical Code as a story · 287 points
HN discussionhttp://spinroot.com/gerard/pdf/P10.pdf
Comment linking /gerard/pdf/P10.pdf
on “Why I Write Games in C (yes, C)”Submitted Rules for Writing Safety Critical Code (2006) as a story · 166 points
HN discussionI can confirm the issues with formal methods. I was working on a new type of locking mechanism and thought I would be smart by modelling it in spin [ http://spinroot.com ], which has been used for these kind of things before. I ended up with a model that was proven in spin, but still failed in real code. Given that's anecdata with a sample size of 1, but still was a valuable experience to me.
Comment linking /
on “Cold Showers: For when people get too hyped up about things”Submitted Code Inflation (2015) [pdf] as a story · 82 points
HN discussion> The idea that simplicity (which I'm pretty sure that nobody in here is using to specifically mean "the lack of cyclomatic complexity") can be measurably improved but that correctness cannot is incorrect. Have you seen a program that comes with a formal proof of correctness? I have. And boy, they are really simple. The end result can be complicated. But the program is broken up into small, simple, easy-to-understan…
Comment linking /
on “Simple, correct, fast: in that order”Submitted Rules for Writing Safety Critical Code as a story · 61 points
HN discussion> It is not impossible to prove, and verify mechanically, that a particular program halts. OK, let's put that to the test. Here is a particular program: let x = 6 let y = 3 while true: if y>x then halt if is_prime(y) and is_prime(x-y) then x = x + 2 y = 3 else y = y + 2 endif Can you tell me if it halts or not? > The state of the art is not up to proving every desirable property of every program that we would like t…
Comment linking /spin/Doc/rax.pdf
on “Diminishing returns of static typing”Submitted Bell Labs, building 2, 5th floor: main occupants for each office over the years. as a story · 27 points
HN discussionThe little interactive graphics language they were writing the compiler for is Pico: http://spinroot.com/pico/index.html http://cm.bell-labs.com/cm/cs/who/gerard/cnn.mpg http://cm.bell-labs.com/cm/cs/who/gerard/pixelface.mpg
Comment linking /pico/index.html
on “Rob Pike: The Best Programming Advice I Ever Got.”Submitted Verifying Multi-threaded Software with Spin as a story · 26 points
HN discussion> https://spinroot.com/gerard/pdf/P10.pdf Originally publicly published in the IEEE Computer journal (doi:10.1109/MC.2006.212): * https://en.wikipedia.org/wiki/The_Power_of_10:_Rules_for_Dev...
Comment linking /gerard/pdf/P10.pdf
on “NASA has a list of 10 rules for software development”Submitted The Power of Ten: Rules for Developing Safety Critical Code [pdf] as a story · 7 points
HN discussionJust to quote the original rationale: > Rationale: Simpler control flow translates into stronger capabilities for verification and often results in improved code clarity. The banishment of recursion is perhaps the biggest surprise here. Without recursion, though, we are guaranteed to have an acyclic function call graph, which can be exploited by code analyzers, and can directly help to prove that all executions that…
Comment linking /gerard/pdf/P10.pdf
on “NASA has a list of 10 rules for software development”Submitted Spin: Formal verification of multi-threaded code as a story · 7 points
HN discussionRead the original and it explains the purpose of each item: https://spinroot.com/gerard/pdf/P10.pdf The original clearly describes that the coding rules primarily target C and attempt to optimize the ability to more thoroughly check the reliability of critical applications written in C. The original author clearly understands what they're doing, and explains lots of other ways to verify C code. For what it's worth,…
Comment linking /gerard/pdf/P10.pdf
on “NASA has a list of 10 rules for software development”Submitted The Power of Ten – Rules for Writing Safety Critical Code as a story · 7 points
HN discussionhttp://spinroot.com/gerard/pdf/P10.pdf (some are more/less appropriate for non-embedded-systems) In general, the answer typically involves formal specification and formal methods that check the code against these specifications, combined with testing and coding standards that result in analysable code. More references: https://www.cs.umd.edu/~mvz/cmsc630/clarke96formal.pdf http://research.microsoft.com/en-us/um/peop…
Comment linking /gerard/pdf/P10.pdf
on “Things I've learned about writing software after 12 years”Submitted PJW's Face as a story · 7 points
HN discussionThe original paper describing and justifying these rules in more detail is at http://spinroot.com/gerard/pdf/P10.pdf , and the official document is at http://lars-lab.jpl.nasa.gov/JPL_Coding_Standard_C.pdf
Comment linking /gerard/pdf/P10.pdf
on “The Power of Ten – Rules for Developing Safety Critical Code”Submitted The Power of Ten – Rules for Developing Safety Critical Code [pdf] as a story · 5 points
HN discussionThey have this famous one - http://spinroot.com/gerard/pdf/P10.pdf ( https://dev.to/xowap/10-rules-to-code-like-nasa-applied-to-i... )
Comment linking /gerard/pdf/P10.pdf
on “I Compiled NASA‘s Workmanship Standards into a Single PDF”Submitted Bell Labs and Peter J. Weinberger’s face as a story · 4 points
HN discussionAdditional reading material: some of NASA's own rules for safe code (with explanations of each! love the stack one, free memory management :P). http://spinroot.com/gerard/pdf/P10.pdf
Comment linking /gerard/pdf/P10.pdf
on “How Is Critical Life or Death Software Tested?”Submitted Rules for Developing Safety Critical Code (NASA) [pdf] as a story · 4 points
HN discussionAbsolutely, but first, CompCert is not really a good example for verification. It is a very small program (roughly equivalent to 10KLOC of C; i.e. 1/5th the size of jQuery), it has taken years of effort by world experts, and they had to cut quite a few corners so your classification of what exactly has been proven is also exaggerated (watch talks by Xavier Leroy [1]). It is more a heroic story of people who climbed…
Comment linking /spin/whatispin.html
on “Correctness – A paradigm for sustainable software development”Submitted Van der Poel's Dead Programs (2017) [pdf] as a story · 3 points
HN discussionA cautionary tale for anyone relying on formal proofs of correctness: https://spinroot.com/spin/Doc/rax.pdf TL;DR: in the 1990s NASA flew an autonomous control system that was formally verified, tested out the wazoo, but which nonetheless failed in flight. [UPDATE] I did not mean to imply that the formal verification failed. It did not. The formal verification worked as advertised. The cause of the failure was much…
Comment linking /spin/Doc/rax.pdf
on “The CompCert C Compiler”Submitted PJW's Face(2018) as a story · 3 points
HN discussion
