2 ms·

Unfortunately, I'm not familiar with Modula-3 or Ada. But I will look into them. Thanks.

• nickpsecurity 10y ago
  Oh wait, if doing Ada, then take this link: http://www.adacore.com/knowledge/technical-papers/safe-and-secure-software-an-invitation-to-ada-2012/ http://www.adacore.com/knowledge/technical-papers/safe-and-s... Remember as you read it that it starts a bit from scratch in the 1980's mainly for embedded, real-time systems that can't fail. The thing to focus on as you skim table of contents or chapter contents is they systematically find the constructions that screw people up, statically prevent them where possible at type system, catch others dynamically by default, and let you drop to unsafety where necessary. The range types (esp existential types), ability to control bit layout, & concurrency safety are old favorites of users in safety-critical space. SPARK is a subset of Ada with extra annotations to help it catch errors statically. It can, with automated provers, show the most common problems can never happen in your code. Here it is: http://www.spark-2014.org/uploads/itp_2014_r610.pdf http://www.spark-2014.org/uploads/itp_2014_r610.pdf http://www.spark-2014.org/about http://www.spark-2014.org/about