Forgetting the concept of postconditions
Ideally, the concept of postconditions (i.e. invariants) is notariously difficult to program : this is where many postconditions are not written. It is much easier to think about any algorithm using only preconditions.
Preconditions are natively implemented by rendez-vous (used as a synchronization mechanism for parallel execution and multithreading). rendez-vous imply a mutex but only between a few participant objects specified in preconditions.
Ideally any pure functional language should be entirely based on preconditions. Preconditions for example all what is needed to support strong type-safety (type is provided by the resulting condition tested when the rendez-vous is met by all participants, so that type inference becomes possible to split an execution path later, because the rendez-vous has generated an fully updated execution context). Type inference can also be extremely efficient because decisions made on the content of the execution context is also delayed up to the point where a precondition for one of the possible execution paths.
Multiple execution paths are also possible from a starting point: this will generate parallel executions, and automatic multithreading, and possibly transparent deployment across remote execution systems available in a computing grid (including collaborations between clients and servers for who will actually run the code -- this means lots of possibilities offered for scalability).
Let's drop compltely postconditions (or invariants which are equivalent), they are not needed. We just need preconditions. The first pure functional language that will be entirely based on preconditions (and only them) will win. It is the dream of mathematicians, theoricians, algorithmists, and the dream (later) of Software Quality Assurance teams. It will also make reuse of code much more versatile.
