7 Jul 2000 guerby   » (Master)

Just a note for those who find "The Future of Programming" advogato post interesting: you might have a look at the book "High Integrity Ada" by John Barnes (Addison-Wesley), it describes a safe "provable" subset of Ada 95 known as "SPARK 95". Also look at the message of Peter Amey in the thread "High integrity software" of the comp.lang.ada newsgroup for some interesting claims.

Formal proofs are in use today with existing languages for non-trivial software, it's just not C/C++ (as the cvsup author John D. Polstra wrote it's "notC" ;-) and what can be called a typical hacker environment and mindset. Needless to say I regret this a lot, in particular the Ada entry of the Hacker's dictionary is highly misinformed ;-).

As for proving with C, it's uselessly hard because the pointer model is pervasive. And for the C++ template model, AFAIK, it does not even enforce interface and implementation separation which is quite essential for scaling up (you need to know all the implementation code to see if your template use will work).

Latest blog entries     Older blog entries

New Advogato Features

New HTML Parser: The long-awaited libxml2 based HTML parser code is live. It needs further work but already handles most markup better than the original parser.

Keep up with the latest Advogato features by reading the Advogato status blog.

If you're a C programmer with some spare time, take a look at the mod_virgule project page and help us with one of the tasks on the ToDo list!