Dr. Dobb's is part of the Informa Tech Division of Informa PLC

This site is operated by a business or businesses owned by Informa PLC and all copyright resides with them. Informa PLC's registered office is 5 Howick Place, London SW1P 1WG. Registered in England and Wales. Number 8860726.


Channels ▼
RSS

Design

It's a Bigger World Than Java and C++


It's no surprise that we haven't heard much about the Tokeneer project. After all, Tokeneer was developed for the U.S. National Security Agency (NSA), an outfit known for keeping things secret. Which makes it even more surprising that not only did the NSA acknowledge Tokeneer's existence, but they released it as open source software.

In a nutshell, Tokeneer is a proof-of-concept of what's called "high-assurance software engineering." Secure software, in other words. Software you can trust. Software that must work correctly or else the consequences could be calamitous. And software that's written in Ada—yes, Ada—and developed using Praxis High Integrity Systems (www.praxis-his.com) Correctness-by-Construction (CbyC) methodology, the SPARK Ada language (www.sparkada.com), and AdaCore's GNAT Pro environment (www.adacore.com). The project demonstrates how to meet or exceed all those things that are necessary to achieve high assurance, such as Evaluation Assurance Level 5 in the Common Criteria (whatever that is). All in all, Tokeneer was created in just 260-person days, and implemented in about 10,000 lines of code. Originally a subset of the Ada language, SPARK Ada is designed in such a way that all SPARK programs are legal Ada programs.

No less than Tony Hoare, Fellow of the Royal Society of Microsoft Research, says that "the Tokeneer project is a milestone in the transfer of program verification technology into industrial application. Publication of the full documents for the project has provided unprecedented experimental material for yet further development of the technology by pure academic research. It will serve as a touchstone to chart and measure progress of the basic science of programming, on which the technology is based." Tokeneer is aimed at both the industrial and academic communities, forming an base for research in program verification and as a high-level teaching aid for educators. You can download the entire Tokeneer project, including requirements, security target, specifications, designs, source code, and proofs at www.adacore.com/home/gnatpro/tokeneer/.

About the same time, IntellaSys (www.intellasys.net) unveiled its 40-core processor designed for embedded wireless, portable, and distributed data processing applications. The 40C18 is an array of 40 fully functional CPUs operating asynchronously, each of the cores a complete computer, with its own ROM, RAM, and interprocessor communication. Together they can deliver up to 26 billion operations per second. So how do you program such a device? Easy. In FORTH. That's right, FORTH. IntellaSys is releasing the processor along with VentureForth, a FORTH-based IDE that includes fully interactive programming, testing, and debugging facilities. VentureForth includes compilers for both Windows and Linux and a simulator for debugging, and contains low-level primitives as well as the high-level tools necessary to map programs across the array of cores in a processor.

"The beauty of this single-chip 40 CPU processing solution is that it is completely programmable—meaning if a spec changes, it is a code issue, not a silicon turn," says Chuck Moore, IntellaSys CTO and inventor of the FORTH programming language. "With 40 cores operating independently on the chip, designers can dedicate groups of them to handle specific tasks. For example, some could be assigned compute-intensive Fast Fourier Transforms (FFT) while others handle wireless connectivity, standard I/O interfaces or drive external memory."

And then there's Python (www.python.org), where the news is that Version 2.6 has been released. Of course, Python 2.6 is really about laying the groundwork for the upcoming Python 3.0, which will be a sweeping redesign of the language. In other words, Python creator Guido van Rossum tells us that "2.6 is the stepping stone from 2.5 (or older) to 3.0. If you want to port your Python 2.x code to 3.0, port it to 2.6 first. Then turn on the '-3' option, which spits out warnings about things you need to change in order to work with 3.0. Clean those up, then run the 2-to-3 source-to-source transformation program, and you should be ready to start the final steps of porting to 3.0."

David Goodger of the Python Foundation adds that, "Python 3.0 goes back to the foundations of Python and fixes them. There are some major changes, for example, to the I/O system and to the text handling (it is Unicode throughout now), but most of the changes are not really revolutionary. Before Python 3.0 began being worked on, various people maintained lists of Python worts and Python mistakes. Guido himself had a list of things he wished he hadn't done or things he wished he had done differently. Python 3.0 is actually taking the opportunity to go back and fix these things. This is something a lot of projects never do."

No, but it is probably something a lot of projects should do.

Jonathan Erickson

Editor-in-Chief

[email protected]


Related Reading


More Insights






Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

 
Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.