LWN.net Logo

We need an RMS, a Linus, or Tridge or Alan or ...

We need an RMS, a Linus, or Tridge or Alan or ...

Posted Mar 9, 2006 9:40 UTC (Thu) by Zelatrix (guest, #5163)
In reply to: We need an RMS, a Linus, or Tridge or Alan or ... by AnswerGuy
Parent article: Some notes from the Coverity survey

I wish I could say that people would use saner languages like Python and Perl for most of their work

However nice those language are (well, Python is anyway), their semantics and dynamic nature make them extremely difficult to statically check, compared to C.

The ultimate language for static-checkability is of course SPARK (see this Slashdot article), which allows you to prove the absence of run-time errors in your program relatively easily and lets you go all the way up to full formal proof of correctness should you so desire (disclaimer: I work for Praxis; the submitter of that article, as far as I know, has no links with the company).


(Log in to post comments)

We need an RMS, a Linus, or Tridge or Alan or ...

Posted Mar 12, 2006 10:24 UTC (Sun) by Xman (guest, #10620) [Link]

How does SPARK's support for static analysis compare to say ML and similar functional languages?

Copyright © 2008, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds