Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.forth > #31231
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Newsgroups | comp.lang.forth |
| Subject | Re: MSP430-Stamp |
| Date | 2014-06-06 01:09 +0200 |
| Organization | 1&1 Internet AG |
| Message-ID | <lmqtan$l3o$1@online.de> (permalink) |
| References | (6 earlier) <7x4n05gtt7.fsf@ruckus.brouhaha.com> <lmfu8n$95f$1@online.de> <7xbnu7ewo7.fsf@ruckus.brouhaha.com> <lmpt18$7k2$1@online.de> <7xzjhrz15q.fsf@ruckus.brouhaha.com> |
Paul Rubin wrote:
>> (e.g. Verilog was originally designed as specification language to
>> formally verify hand-drawn circuits; but it soon was compiled
>> instead).
>
> That's not easy though: Verilog compilers do a heck of a lot of work,
> especially if you consider the "output" to be rectangles, so compilation
> includes place-and-route. Yes it's awesome how well that problem has
> been solved but it's much easier to specify a chip's function (in
> Verilog) than to actually render it.
No, been there, done that. A lot of electric engineers think that the
Verilog compiler can't produce something good and meaningful out of my
mostly straight-forward pretty high-level description (e.g. the b16
processor). I've been told that the synthesis tool won't produce what I'm
intending. I've looked, it did. The compilation is broken into steps, so
that place-and-route is actually a different operation, and BTW all those
steps have equivalence provers to check that they are done correct (formal
verification to compare RTL to netlist, and Layout vs. Schematic (LVS) to
compare the place&route result to the netlist.
>> Or better: Make a formal language that allows you to specify your
>> problem easily, i.e. a DSL.
>
> Specifying the problem is of course not the same as solving it. Think
> of two Forth words (predicates on integers):
> : w1 ( n -- flag ) .... ;
> : w2 ( n -- flag ) .... ;
> You can specify a property called "equivalence" on two words with this
> signature: they are equivalent iff for all inputs they produce the same
> output. For example, w1 and w2 might both test whether n is a prime
> number using completely different algorithms. The equivalence spec
> captures that they both compute the same thing. Now imagine you've
> got a function that operates on fragments of machine code:
>
> : optimize ( xt1 -- xt2 )
> \ SPECIFICATION: xt1 and xt2 are equivalent ... ;
Ouch. If you had followed our discussion with Andrew (representing the GCC
team, a bad job he has here ;-), you'll immediately see that "equivalent" is
something that is pretty hard to define. Because there are these
"undefined" results...
Take your prime number example above: For calculating RSA key primes, you
use a probabilistic test for prime. This probabilistic test will never
report a prime as non-prime, but will give false positives. So all you do
is to repeat the test until you are sufficiently sure that it is a prime.
There is still a (small) likelyhood that you are wrong.
This stuff is used in crypto software. The specification for RSA of course
is "For an n bit key choose two different randomly chosen prime numbers p
and q with n/2 bits each". Of course the programs formally never will meet
that spec, because a probabilistic prime number test has a likelyhood of
failure.
> This is a compiler optimization pass that takes a chunk of code and
> returns an "improved" chunk that does the same thing. Maybe it's
> "buggy" in the sense that the new code is slower than the old code
> rather than faster,
That wouldn't be hard, just specify that there is a total order, and the new
code has to be at least as fast as the old code.
> but if the equivalence spec is verified, the
> optimization can't introduce an actual wrong-code bug. This is
> basically how CompCert works: it has a series of code transformations
> that are all verified to satisfy input-output equivalence in the above
> sense. So we get papers like http://mehrdadafshari.com/emi/paper.pdf
> which introduce methodology that finds hundreds of codegen bugs in GCC
> and LLVM, but not a single one in CompCert.
I'm surprised that the Clang and GCC team actually confirmed and fixed 2/3
of these bugs. The remaining are probably all "invalid" ;-).
> What's not so easy, of course, is generating those transformations and
> equivalence proofs automatically, given just the spec. Humans are still
> in the loop.
IMHO, you are picking something that is a very good target for formal
methods, because it actually does an equivalence transformation: The
optimizing backend of a compiler. I've argued about not using Formality (a
RTL vs. netlist comparison tool) on a project that had a very tight
deadline, because it actually verifies that the Verilog compiler isn't
producing bullshit, and we were confident that the Verilog compiler was good
enough - never found a miscompilation in years.
And I'm really scared that this sort of tool is not available for verifying
software compilers. There are two reasons for having such a tool:
1. Debugging the compiler (and they need a lot of debugging), and
2. checking binaries for hidden backdoors (see Ken Tompson's stone-age paper
about compiler security...)
>> The zero-defect example that they list in the end of the article is just
>> 10kLoCs, and it was written quite fast (38LoCs/day is really fast).
>
> The second article discusses the Mondex wallet which is around 100 KLOC.
> The Tokeneer code is here, btw: https://www.adacore.com/sparkpro/tokeneer/
>
> I think the 38 LOC/day might just be the coding phase of the project,
> which is a somewhat bogus because of the longer-than-usual design and
> prototype phase. To compare process productivity you really have to
> compare start-to-finish times of entire projects. But, I don't mind the
> idea that a high-assurance process takes longer than a lolcat process
> (where it's reasonable to expect 100+ loc/day with good coders). The
> interesting thing is that these verification methods were known in the
> 1970's or 80's and were considered impractical then, but they're
> relatively accessible now, and yet most programmers still think they're
> impractical (rather than just somewhat specialized).
>
>> Nope. Spilling keys is just as bad as e.g. not detecting a MITM attack.
>
> Of course spilled keys are worse: they enable the MITM attack whether or
> not the attack is present in the protocol implementation, and they
> enable it for all future sessions that use the same authentication key,
> even if the implementation is patched. And if the protocol lacks
> forward secrecy or accidentally persists keys (think of session caches),
> the spilled key can even reveal past traffic from before the MITM got
> in.
Ok, I think of non-forward secrecy protocols as broken anyways ;-). That is
because there are other ways to get a constant key than just a bug in the
implementation...
>> The assumption that Java helps you to avoid crazy stuff IMHO is
>> completely unfounded.
>
> It avoids so-called "nasal demons" of which spilling keys in Heartbleed
> was an example.
Are you sure of that? The problem with Heartbleed and OpenSSL is that it
had its own malloc, because someone found a reason to avoid using the
system's malloc - that's why tools like Valgrind didn't find a problem. Now
guess if this sort of stupid design decision would have been made in Java:
Instead of using Java's native objects to store data, the hypothetical
jOpenSSL developers would have allocated 64k ByteArrays and implement their
own storage management on top of those...
Yes, really, that's the sort of code quality we are discussing here. It's
like you use Forth, and stop passing addr u as buffers because you think
this takes too much stack space. And then you end up with a buffer
overflow... People who try that sort of stuff will manage to expose their
keys in Coq. Provable (if you add the rule to show the proof ;-).
>>> told me they really do need a lot of the bloaty-looking code in it, that
>>> deals with buggy browsers, weird certificates, etc.
>>
>> They are taking the Postel principle way too far here. A widely used
>> encryption software can be used to sanitize the Internet from these
>> things: Fail on the weird certificates, let the buggy browers fail
>
> Like most businesses they are more interested in satisfying their
> customers than "sanitizing the internet". If each rejected browser or
> certificate results in angry customers and piles of support tickets, and
> those browsers and certs work perfectly well with other servers, then
> they have strong motivation to also handle those browsers and certs.
This is a hypothetical situation, the real situation is that the other SSL
implementations usually choke on a lot more certs than OpenSSL... the
Frankencert study unfortunately shows that the other SSL implementations
choke by *accepting* those broken certificates:
https://www.cs.utexas.edu/~shmat/shmat_oak14.pdf
That is of course worse than accepting a just weird certificate...
The reason here is probably that these other SSL libraries are used in web
servers, and those rarely have to check certificates, so the bugs slip
through.
>>> Nobody is willing to install desktop apps these days.
>> That's not true. A lot of people do install things like Google Drive
>> and DropBox, where the brower can't do everything....: It makes their
>> different devices interoperate without problems.
>
> Hmm, yeah, I forgot about that due to being suspicious of the downloads
> and not using a lot of devices, plus having relatively slow internet and
> knowing how to use upload programs. I just use git or rsync for
> synchronization.
Yes, my reaction to the first person mentioning Dropbox (for exchanging
stuff submitted to our Forth Gesellschaft journal) was "use a DVCS, please!"
But the Dropbox model of watched folders and automatic sync is really a lot
easier for mere users.
>> The fact that sendind all your data through Google means sending all
>> your data through the NSA is something people like to ignore.
>
> Even if it's not going to the NSA, it's still going to Google.
Yes, but at least Google has no prisons and no killer drones (they have
bought a maker of the latter recently, though).
>> the far easier SSH model ("remember the first contact") is already far
>> better than the CA system. It is not perfect, but at least an
>> attacker must be persistent ("captive environment"), and really
>> intercept every connection.
>
> I don't think so, it's bad enough if they intercept just the first
> connection, if that's the only connection. E.g. you're in a wifi cafe
> with MITM and you connect to a new site for the first and only time.
> Even if you connect again later and discover the changed key, what are
> you going to do about it? What happens if you connect to an sshd that
> you use regularly, except this time the key has changed? Most of us
> just figure the sysadmin has changed the key for some reason, and say
> "yes" to accept it. Not good.
Ok, the latter is the key migration problem: I've solved that; it doesn't
require a certificate authority, but can be made 100% secure. The wifi cafe
problem isn't solved in SSL, either (or, let's say: It is broken. What do
you expect the MITM wifi box from the Chinese government will do when you
use SSL? It will present you a certificate signed by the Chinese
authorities, which is part of the root certs in your browser... The
Iranians needed to hack Diginotar to get such a wildcard cert - but they got
it ;-).
>> Some CAs have issued wildcard certificates for exactly those boxes
>> that do DPI and filter the traffic for captive environments (usually
>> inside a company or a totalitarian country).
>
> I don't think any preinstalled CA's can admit to that and survive.
They did. They simply were too big to fail, or for other reasons couldn't
be revoked (like Verisign and GoDaddy who provides wildcard certs for
coroporate MITM firewall suppliances). If you throw out Verisign and
Godaddy, the Internet goes dark. If you take the Chinese authority cert out
of the root cert list in the browser, you can say goodbye to the Chinese
market.
> The
> ones inside companies involve browsers on company computers, configured
> by the company to accept the MITM certificate. Since the company also
> controls all the software on the computer, SSL MITM isn't particularly a
> point of vulnerability.
Yes, that's the idea, and that's how it should work. But BYOD is a trendy
thing, and the makers of those boxes have found ways to deal with it. Scary
ways.
> The CA system works reasonably well for its intended purpose, the online
> shoe store model where compromising millions of sessions (by
> intercepting traffic at the server) is disastrous but compromising a few
> individual sessions is only annoying (person has to get a new credit
> card, bank has to pay for any monetary losses and they build occasional
> such losses into their existing cost structure). It's more problematic
> in the gmail model where each session is its own potential spy story
> that could start a war or whatever. Extensions like TACK can indeed
> help with this.
The Gmail thing fortunately is the one which is easier to solve: The people
you are communicating with are social contacts. People where you can
actually verify their IDs or establish a trust path through other social
contacts. The shoe shop model actually also gives you a way to deal with
the cafe wifi single connection situation: You have to use a communication
with a known and trusted third party, your bank, to complete that
transaction.
The thing that is broken with the CA system is that one single signature
from one of the 600 CAs (including "Turktrust" and the Chinese government,
and the biggest CAs are all subject to NSLs) gives you "trust".
The model I have in mind is that you get trust by asking others, not by
asking the probably MITM-attacked communication partner. The way net2o
addressing works means that when you tell me "go to this site" or "talk to
this guy", you are already giving me the pubkey of the site or the guy,
because you have used it, and stored it in your bookmarks or address book.
>>> there are faster ECC implementations than Donna now.
>> Which one? I'm deliberately using Dan Bernstein's Ed25519 curve,
>
> There are several people who claim to have them, I haven't tracked
> specific implementations but there might be some info in the curves
> mailing list archive at moderncrypto.org. The messaging list on the
> same site would be a cool place for you to send something about net2o,
> by the way.
Yes, thanks. Seems to be rather new.
>> Non-conclusive logic: Interactive languages makes it more fun to
>> squash out bugs.
>
> You know, I don't really find this. I find interactive debuggers
> helpful (I know that you don't). Interactive languages are nice when I
> don't understand the API of some library I want to use, so I want to try
> stuff and poke at it. For code where I understand what's already there,
> careful coding and/or TDD seems to help more than interactivity.
Ok, then make that an issue of taste. I find "careful coding" conter-
productive and not fun. Usually, I write way too much stuff when "carefully
coding". I'm very nervous when making big changes, I prefer to make small
changes and then check. Check can mean run a prepared test (that's usually
when refactoring), or test interactively (that's when I test newly written
stuff). Once it's solid enough and I understand what I'm doing, I can start
putting regression tests into a file.
Trying stuff and poking at things happens IMHO quite often.
>> Maybe you want the client to renegotiate so that you can inject some MITM
>
> You're in trouble if any version of the protocol allows MITM.
Sure. The thing is that this sort of bug is not caught by some typechecking
or such. Just today, we had another OpenSSL bug in this class - mess with a
connection during setup so that both sides will switch to a very week
encryption.
>> Ok, two things here: If you receive a packet that doesn't decrypt
>> well, you have to drop that packet and continue as if there wasn't
>> anything. Otherwise, you make it dead easy for someone to DoS you.
>
> Ehh, if they can mess with packets they can already DOS you.
You know, you can fake the sender on the current Internet...
>>> QuickCheck itself generates the values... using Haskell's
>>> fine-grained type system to determine the possible good values.
>>
>> Sounds good. ... A question would be: Could we adapt that sort of
>> testing to Forth? Maybe together with an analytical compiler to
>> produce efficient code? That compiler performs enough analysis of the
>> code to know the stack effect, so it can compare that to the
>> documentation (which is a specification).
>
> Typical Forth stack comments probably don't have enough info to be much
> help: for example, the test generator might not figure out that "addr u"
> is supposed to be a character string. And I get the impression that
> wrong stack effects already aren't a frequent source of bugs in Forth
> code (are they?)
No, not really. But if you want to go down from 1 bug per kLoC to 0.01 bug
per kLoC, you may include those bugs as something you might want to check,
too.
> and they can usually be checked statically without any
> tests. Peter Knaggs' PhD thesis (it's online someplace) discusses how
> to write more specific Forth signatures that sort of resemble Haskell
> types. Maybe that's worth looking into for test generation.
Yes, that sort of thing would be necessary. Some people use "addr len"
instead of "addr u" to specify strings, just to make clear that u is not
just an unrelated integer. There were some discussions to use "addr len" in
Forth200x, but we dropped that.
>> Usually, the thing with Forth's one-liners however is that you have
>> complete oversight.
>
> Well with QuickCheck (or other testing) you exercise the entire call
> tree under the one-liner.
This "complete oversight" stuff is more about that you are putting things
together which are all trustworthy.
>> No, the point here is that you need your object under test to develop
>> the tests, see your Haskell thing above. The opposite of "write the
>> tests first" is not "don't write any regression tests".
>
> You can still write the tests first, and doing that helps make the
> design testable, it's not boilerplate filling. I find it useful for
> some types of code (mostly in Python).
Maybe. The network and encryption stuff I'm doing makes writing test first
pretty hard, because the expected output of some cryptographic function is
not something you can easily calculate. E.g. take the key renewal: You
need to revoke the old key using some signatures and a diffie hellman
exchange for the magic that proves that you made that key; and provide the
new key, which also needs a signature to prove you own it.
The way to deal with that is that I write the code to generate and to check
the revocation together, and then generate revocations, fuzz them, and check
them. The unmodified must pass, any change must cause a failure.
This is incremental: Of course I start with an incomplete renewal, and then
add signatures and checks until it is complete.
--
Bernd Paysan
"If you want it done right, you have to do it yourself"
http://bernd-paysan.de/
Back to comp.lang.forth | Previous | Next — Previous in thread | Next in thread | Find similar | Unroll thread
MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-29 21:35 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 19:09 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 19:13 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-29 23:00 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 20:25 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 20:23 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 22:15 -0700
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 15:13 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 13:51 -0400
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 21:08 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 12:22 -0700
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 21:41 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 13:28 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 17:55 -0400
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 16:29 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 14:18 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 18:07 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 17:24 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-02 11:10 +0200
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-02 10:57 +0000
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-02 13:34 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 20:10 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-29 20:29 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 21:02 -0700
Re: MSP430-Stamp "Rod Pemberton" <dont_use_email@xnothavet.cqm> - 2014-05-30 04:05 -0400
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-05-30 15:13 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 19:57 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-29 23:32 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-29 21:07 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-30 02:39 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-07-17 12:40 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-17 16:08 -0400
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-18 00:06 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-07-18 08:22 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-18 23:42 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-18 18:28 -0400
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-19 01:41 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-18 19:48 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-07-18 16:59 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-07-19 14:30 +0200
Re: MSP430-Stamp Gary Bergstrom <forthprgrmr@gmail.com> - 2014-07-19 08:23 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-07-21 10:42 +0200
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-30 03:03 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 07:47 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-31 11:36 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-31 09:34 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 10:09 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-31 10:52 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 01:28 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 22:41 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 02:00 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 23:07 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 03:13 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 07:15 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 12:33 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 09:45 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 13:10 -0400
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-06-01 18:38 +0200
Re: MSP430-Stamp babruehl@gmail.com - 2014-06-01 11:40 -0700
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-06-01 11:13 +0200
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-01 09:50 +0000
Re: MSP430-Stamp HaveANiceDay <HaveANiceDay@NoSpam.invalid> - 2014-06-01 12:47 +0200
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 04:05 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 12:39 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 10:00 -0700
Re: MSP430-Stamp babruehl@gmail.com - 2014-06-01 11:45 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 14:57 -0400
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-01 12:01 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-01 15:12 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-30 03:12 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-30 14:02 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-31 03:33 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 07:19 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-05-31 12:01 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 09:15 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 13:51 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-05-31 14:20 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 14:51 -0700
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-05-31 16:22 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-01 01:33 +0200
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-05-31 17:31 -1000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 21:48 -0700
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-05-31 19:12 -1000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 22:25 -0700
Re: MSP430-Stamp stephenXXX@mpeforth.com (Stephen Pelc) - 2014-06-01 09:45 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-01 04:16 -0700
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-01 08:51 -1000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-05-31 21:03 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-01 21:17 +0200
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-04 22:46 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-05 13:27 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 08:39 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-05 16:10 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 11:10 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-05 19:52 +0000
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-05 23:25 +0200
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 15:02 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-06 10:56 +0000
Correct Software and Specifications (was Re: MSP430-Stamp) Paul E Bennett <Paul_E.Bennett@topmail.co.uk> - 2014-06-09 09:59 +0100
Re: MSP430-Stamp mhx@iae.nl - 2014-06-05 14:30 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-06 10:59 +0000
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-05 15:57 +0200
Formal specifications etc. (was: MSP430-Stamp) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2014-06-05 15:34 +0000
Re: Formal specifications etc. Paul Rubin <no.email@nospam.invalid> - 2014-06-05 11:48 -0700
Re: Formal specifications etc. anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2014-06-05 19:46 +0000
Re: Formal specifications etc. (was: MSP430-Stamp) Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-05 23:02 +0200
Re: Formal specifications etc. Paul Rubin <no.email@nospam.invalid> - 2014-06-05 14:15 -0700
Re: Formal specifications etc. rickman <gnuarm@gmail.com> - 2014-06-05 17:33 -0400
Re: Formal specifications etc. Paul Rubin <no.email@nospam.invalid> - 2014-06-05 15:32 -0700
Re: Formal specifications etc. Andrew Haley <andrew29@littlepinkcloud.invalid> - 2014-06-06 04:00 -0500
Re: Formal specifications etc. (was: MSP430-Stamp) albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-06 11:05 +0000
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-05 11:01 -0700
Re: MSP430-Stamp Bernd Paysan <bernd.paysan@gmx.de> - 2014-06-06 01:09 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-05 22:01 -0400
Re: MSP430-Stamp stephenXXX@mpeforth.com (Stephen Pelc) - 2014-05-31 16:47 +0000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-05-30 12:11 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-06 12:54 +0200
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-02 11:39 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-02 12:15 -0400
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-03 10:26 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-03 12:18 -0400
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-02 10:04 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-03 11:51 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-03 13:33 -0400
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-06 13:02 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-06 17:31 -0400
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-06 16:30 -1000
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-06 22:52 -0400
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-07 11:58 +0000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-07 11:40 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-07 20:01 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-08 16:05 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-08 22:28 -0400
Re: MSP430-Stamp Gary Bergstrom <forthprgrmr@gmail.com> - 2014-06-08 20:36 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-08 21:38 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-09 14:36 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 02:45 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 03:18 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-09 15:57 -0400
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-08 16:20 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 20:42 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 21:05 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-04 10:43 +0000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 21:28 -0700
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-03 22:43 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 23:31 -0700
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-04 04:13 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 01:41 -0700
Re: MSP430-Stamp Paul Rubin <no.email@nospam.invalid> - 2014-06-03 01:51 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-03 16:19 +0100
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 09:14 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-03 13:19 -0400
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-03 07:43 -1000
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-03 20:56 -0700
Re: MSP430-Stamp albert@spenarnc.xs4all.nl (Albert van der Horst) - 2014-06-04 10:51 +0000
Re: MSP430-Stamp VisualForth <babruehl@gmail.com> - 2014-06-04 04:06 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-06 21:26 -0400
Re: MSP430-Stamp "VisualForth.com" <babruehl@gmail.com> - 2014-06-06 20:40 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-07 03:18 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-07 04:35 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-07 12:01 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 03:47 -0700
Re: MSP430-Stamp Mikael Nordman <oh2aun@gmail.com> - 2014-06-09 09:28 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 07:35 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-11 10:43 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 15:52 -0700
Re: MSP430-Stamp Coos Haak <chforth@hccnet.nl> - 2014-06-12 02:06 +0200
Re: MSP430-Stamp "Elizabeth D. Rather" <erather@forth.com> - 2014-06-11 15:13 -1000
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-12 02:16 -0700
Re: MSP430-Stamp Mikael Nordman <oh2aun@gmail.com> - 2014-06-11 12:56 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-09 16:46 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-09 03:49 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-09 09:47 -0700
Re: MSP430-Stamp Rikard Lang <rikard.lang@gmail.com> - 2014-06-09 23:16 +0200
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-10 07:48 -0700
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 07:23 -0700
Re: MSP430-Stamp David Schultz <abuse@127.0.0.1> - 2014-06-11 18:00 -0500
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-12 02:14 -0400
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-12 02:13 -0700
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-12 13:04 -0400
Re: MSP430-Stamp David Schultz <abuse@127.0.0.1> - 2014-06-12 18:06 -0500
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-12 19:29 -0400
Re: MSP430-Stamp David Schultz <abuse@127.0.0.1> - 2014-06-13 18:48 -0500
Re: MSP430-Stamp Mark Wills <markwills1970@gmail.com> - 2014-06-11 07:26 -0700
Re: MSP430-Stamp visualforth@rocketmail.com - 2014-06-11 10:45 -0700
Re: MSP430-Stamp JUERGEN <epldfpga@aol.com> - 2014-06-13 00:03 -0700
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-18 11:11 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-06-18 05:27 -0400
Re: MSP430-Stamp Matthias Koch <matthias.koch@hot.uni-hannover.de> - 2014-06-18 12:29 +0200
Re: MSP430-Stamp rickman <gnuarm@gmail.com> - 2014-07-17 16:09 -0400
csiph-web