What is the most interesting program that you've seen written with Modula-3?

I'll just talk about my programs. I wrote the second program (after Next Computer's) direct-manipulation user interface editor. And I wrote the Obliq distributed programming language, which was heavily based on Modula-3's network objects.

Have you ever seen the language used in a way that was not originally intended? If so, what was it? And did it or didn't it work?

Not really; we intended to support type-safe systems programming and that is what happened. It's possible that we missed some opportunities, however.

Why do you think that the language hasn't been widely adopted by industry, but is still influential in research circles?

Basically, competition from Java. Java had all the same main features (objects, type safety, exceptions, threads), all of which also came from the same tradition (and I believe they read our tech reports carefully...). In addition, Java initially had innovations in bytecode verification and Web applets, and later had the full support of a large company, while we were only supporting Modula-3 form a research lab. I believe the module system in Modula-3 is still vastly superior to programs such as Java, and that may explain continued interest.

Do you still use Modula-3 today? Is the language still being contributed to and updated?

While Modula-3 was my all-time favorite language, I stopped using it after leaving DEC. I used Java for a short period, and today I occasionally use C# and F#.

How do you feel about statements such as this in Wikipedia: "Modula-3 is now taught in universities only in comparative programming language courses, and its textbooks are out of print"?

It's probably accurate!

According to Wikipedia, the Modula-3 "standard libraries [were] formally verified not to contain various types of bugs, including locking bugs." Why was this?

Type safety gets rid of a lot of silly bugs, but the main class of bugs it does not prevent are concurrency bugs. The expectation for Modula-3 libraries was that they would have a complete description (in English), of exactly what each procedure did and what it required. There was social pressure at the time to make these descriptions very precise. Some were so precise that they were amenable to formal verification. This was considered important for some base libraries, particularly in terms of locking behavior, because locking bugs were not captured by the type system, and were the hardest to debug.