If you want to learn Forth, I strongly recommend reading Leo Brodie's "Starting Forth" first.
http://www.forth.com/starting-forth/
However, do not stop there. The proceeding text only details the mechanics of coding in Forth; the actual act of solving real problems
in any programming language involves practice and acquired skill. Pay particular attention to
patterns of coding practices, program structure, etc. Over time, you'll notice that, even though they might do completely different things, routine A and routine B might be structured so similarly, that you just
know that some underlying principle applies to both.
These kinds of observations give rise to things such as
design patterns (see
http://c2.com/cgi/wiki?DesignPatternsBook), which are elements of design concentrating how abstract data types and/or objects relate to each other.
The same concept applies to
coding as well -- a collection of Forth-related
coding practices is contained in the book
Thinking Forth, also by Leo Brodie, and also online:
http://thinking-forth.sourceforge.net/
I should point out that the patterns contained in Thinking Forth don't always apply just to Forth; many of the concepts are so general that they apply to other languages as well.
In fact, many of the practices you read about today in so-called "agile" development practices have been formalized in Thinking Forth decades before "agile" became a house-hold word. The only real recent innovation in the agile community is that of
test-driven development, but TDD's practicality could come about until object-oriented programming and polymorphism became common-place and easier to use in languages. But that's OK, because you can also program iteratively using formal methods too.
In fact, all Forth programmers, to some extent, already employ formal methods in their programming without actually realizing it. The foundation for all formal verification of software, the
Hoare Triple, looks like this:
{P} S {Q}. This is saying two things:
1.
IF condition Q is true (because we measured it, or because of some observed artifact elsewhere), when we know that the condition P
must be true because of S.
2.
IF condition P is true, then because of S, we know that Q must also be true.
This should be setting off alarm bells all over the place to those who code in Forth here; as Forth coders, we tend to write these kinds of things differently:
: S ( P -- Q ) ... ;
Yes, that's right, the humble stack effect notation is really a degenerate form of a Hoare Triple.
What makes formal methods "formal," of course, is their reliance upon first-order logic and its associated notation instead of single letters. For example, ANSI Forth's COUNT word has the documented effect:
( c-addr1 -- c-addr2 u )
However, this doesn't say anything truly useful: given a character address, return a character buffer. The relationship between these two entities remain unclear -- you have to read the full body of the description for COUNT to realize what's happening.
Were we to use formal notation, it'd be rewritten something kind of like this:
( caddr-1 -- caddr u, where: caddr-1 c@ u = caddr-1 isFetchable? and )
This explains to us the following:
* caddr-1 stores the character 'u'. Now, as you'll undoubtedly learn in the Starting Forth book, (caddr u) pairs are used to describe character buffers, so you'll understand that 'u' must be a length.
* caddr is 1 greater than caddr-1, and therefore, _this_ is the actual start of the character buffer. Hence, a "counted string", when stored in RAM, appears as a length byte followed by that many bytes of data.
* 0 <= u < 256 (for an 8-bit byte machine), so no buffer can exceed 255 bytes.
* We find that caddr does NOT need to be memory accessible!! For example, on a Commodore 64, $D000-$DFFF is the I/O space. Suppose we happen to store a zero-length buffer at $CFFF. COUNT will still work as expected -- it'll return a valid 0-length buffer on the stack. But, caddr will be $D000, which is pointing at I/O, not RAM.
So, in a nice, concise format, we have described the entirety of what COUNT does, and with this, we can actually prove an implementation conforms to this interface description. Once this proof has been made, the "stack effect" for the word can be taken as truth, and thus, you now can use it to reason about whatever other Forth code you've written that uses it.
Interestingly enough, some folks actually use COUNT as a means of iterating over every character in a string. According to the weakest precondition and postcondition of COUNT, this is well within its normal realm of use, even though the name COUNT implies it wasn't its intended purpose.