How to make the static represent the dynamic?

Seemingly a fair number of bugs in software stem from the complexity of the dynamic nature of runtime: concurrency issues, rare this-then-that-equals-infinite-loop issues, etc. How can a programming language be designed to try to make the static source more directly either reveal the runtime possibilities, or better constrain them to avoid confusion and thus bugs? Some languages do that by choosing better defaults (Erlang, Haskell, etc.) but obviously they don't constrain away all the differences between source and runtime. Presumably no language could, and still be all that useful. But how close could one usefully get?

Sure, having an IDE that generates UML interaction diagrams for all the possible concurrent API call interleavings might in some sense help, but tools along those lines really feel like mistakenly allowing grape juice in the room at all.

Since sundry tools for miscellaneous languages do already exist, I am more interested in how to refine/constrain core languages rather than ancillary tools. But, how could one at least provide tools to help e.g. automatic deadlock detection for CSP, or design-by-contract to effectively constrain the runtime state?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Proof-carrying code?

...on a higher level.

Integrate more powerful reasoning tools into the core language, eg. type inferencers are stupid theorem provers, if you look at them funny. You can do a lot in type-level Haskell, but from an (automated) theorem proving point of view it's pretty crude.

Just an idea.

Edit: hey, this is being discussed in the Monad.Reader thread!

Unimportant aside

Actually, type checkers are theorem checkers and type inferencers are theorem reconstructors (or something like that), you start with the proof (the code) and end up with the theorem that you are proving (the type).

Yep...

...and there are older threads on Why Dependent Types Matter, Djinn: A Theorem Prover in Haskell, for Haskell which also refers to Oleg Kiselyov's in-place "de-typechecker", The Reasoned Schemer (it's underappreciated, IMHO, that one of the Kanren sample applications is the Hindley-Milner type-inference relation—a typechecker, type-inferrer, and intuitionistic theorem prover all in one shot)! Also see Lightweight Static Capabilities, which has a strong dependent-type flavor but is applicable in languages such as O'Caml and Haskell today.

Here's the thread that really made it abundantly clear that my computer science education was woefully out of date and enthralled me enough to spend many hundreds of dollars on Amazon playing catch-up: Python Metaclass Programming. It contains a priceless exchange between Tim Sweeney and Frank Atanassow that is sufficient grist for years of study. See also Tim's post on Ontic, which is still something that I wish to understand some day.

Finally, see this thread on automated theorem proving, where I sing Coq and the Coq'Art book's praises, as well as reveal my own ignorance of the subject. :-)

Displaying interleavings

Sure, having an IDE that generates UML interaction diagrams for all the possible concurrent API call interleavings might in some sense help...

For anything other than trivial concurrent programs, the sheer number of possible interleavings is likely to make an approach like that infeasible. Granted, it'd probably be helpful for those trivial programs, since there still tend to be subtleties in even "trivial" concurrent programs. But for any non-trivial concurrent program (more than a few threads, with more than a few interaction points) you really need some way to prune the space of interleavings that will be displayed. The most reasonable approach I can think of is to have the programmer describe what kind of interleavings are acceptable, and then have the IDE (probably via model-checking ala Java Pathfinder) display only those interleavings that don't provide the desired properties (i.e. counterexamples).

Re: triviality

I heartily concur; it was said somewhat tongue-in-cheek. I do like your idea of QuickCheck style presentation of instances that break the defined desired behaviour.

Not my idea

I do like your idea of QuickCheck style presentation of instances that break the defined desired behaviour.

I agree that it's a good idea. Unfortunately, it's not original to me :-/ The model-checkers with which I'm familiar (in particular the CSP model-checker, FDR, with which I have the most experience) generate counterexamples whenever a property check fails. In the case of FDR, that failure might be with respect to something as simple (ha!) as deadlock, a complex constraint on the allowable system traces, or even refinement of an abstract system model by an implementation-level model. In each case, FDR provides one or more traces which can lead to the undesirable behavior, and the ability to explore the traces of individual system components to better understand how the system-level trace arose.

Responding to self

The closest would be things like CSP+checker because potentially you are just writing regular CSP with no extensions, and the language inherently allows checkers to "easily" prove things like no deadlock?

You can have checkers for other languages but those maybe any of: more computationally expensive, even intractable, or require you to annotate your core language with extra fu e.g. like JML? Static checkers like EscJava or FindBugs might tell you when you are doing smelly things. But it doesn't seem like these are going to tell me "I've proven you have no deadlock."

Maybe things like skeletons for parallelism are good because they try to get the "high level" programmer out of the business of dealing with all the complexity and risk inherent in parallel / concurrent programming. I wonder if the skeleton approach gets much respect? E.g. don't know of many Java folks really going in that direction in any large sense. There was JaSkel but that doesn't seem to have ever turning to a real living, maintained project.

Not that Java is the be-all-end-all. :-)

So I think there are degrees to which a language & development environment can help:

  1. Syntax and semantics inherently don't let you write dangerous things; they are trying to use the right defaults. CSP+checker proving no deadlock. Timber+checker proving no deadlock. Haskell's separation via monads. Erlang's single-assignment. Light-weight share-nothing processes. But seemingly there isn't a single language that has wrapped up the great variety of goodness into one package?
  2. If you can't use a language that is inherently safe, you can try to restrict yourself to a safe(er) sub-set.
  3. And/Next, try to get static checkers and lots of testing in place. You have unfortunately stepped over the line from "kinda proven" into "kinda all just probability modulated by experience: test a lot!"
  4. Finally, you are just doing regular old shared-mutable-state-concurrency in Java, you don't even know about FindBugs, and all bets are off.

mutating types

Mutating types could be a solution. For example, a file is of type

open

after opened successfully, and of type

closed

after closed successfully.

The only correct transition of states for a file is

open -> closed -> open 

If it was possible to mutate a file type from open to closed and vice versa, some errors would easily be caught at compile-time.

I think this applies in a great variety of problems. For example, it applies in nullable types (think of 'null' as 'closed' and 'non-null' as 'open').

I think the solution can actually be applied in all algebraic types, because null/non-null or open/closed are algebraic types themselves.

You need linear or uniqueness types

to avoid the following nastiness.

Closed c;
Closed d = c;       // d is an alias for c.
Open c = c.open();  // migrates the type of c.  But what of d?

In the above pseudocode, d has type type of closed, but the underlying value has been migrated to open.

Alternatively, you need monotonic type migration--type migration is sound when a value acquires a new type which has stronger invariants then the old one--but the closed/open/closed cycle is obviously non-monotonic.

The so-called four out of five rule may come into play.

Achilleas and I had much

Achilleas and I had much this discussion a while back, using phantom types to encode openness/closedness, and extending to GADTs to allow sensible isOpen/isClosed predicates.

Do you have a link to that

Do you have a link to that discussion? I'm interested in reading about the solution you came up with.

Link

I think it's this thread.

Thanks, that's the one I had

Thanks, that's the one I had in mind. I don't know that my own comments were as hugely helpful as might be hoped for there.

When is the release party?

It all sounds (a bit over my head but still) very compelling. What is the latest on that sort of thinking in terms of actually available languages? Many thanks for any refs.

Two parts (GHC) Haskell to

Two parts (GHC) Haskell to one part Clean would get you it - I don't know off-hand of a language that has all the necessary features (anyone else?), although I imagine I could write an interpreter for an explicitly-typed intermediate lang based around System FC that handled it reasonably easily.

There's a chapter in ATTaPL on substructural type systems that covers linear types, I'm not aware of any particular interactions between them and GADTs that would prevent combining them in the obvious way.

Vault

I don't know off-hand of a language that has all the necessary features (anyone else?)

Vault can do this sort of stuff, via a linear type system.

Presumably one could do it

Presumably one could do it with Coq, although I don't have much experience with it offhand.

I don't know that you could

I don't know that you could without an interpretive layer - I'm not aware of Coq supporting substructural typing directly, though I'd be happy to hear I'm wrong.

Nope...

...but it'd be nice to developer a certified compiler for a language with substructural typing in Coq. :-)