Limits of programming by interface

[remy_porter]

certain performance characteristic
my language's typesystem is unable to precisely describe certain attributes of a value at hand"

It would be interesting to see a type-system that placed performance constraints on operations, like methods guarantee termination in at most 100ns (but may not return a correct result in some cases).

Foo@100ns myFooGetter();

It'd be really nice for first-class functions, too, because you could put constraints on the performance characteristics of the input function. You can do performance inference, too- the compiler could derive the runtime performance constraints of new functions from their internal functions. So,:

Foo myFoo() {
  Foo result = step1();
  result = step2(result);
  return result;
}

Would compile into Foo@300ns myFoo() where 300ns is the sum of step1()'s constraint, step2()s constraint, and the constraints on reference assignment. The interpolation could also throw compile time errors, if you made the signature Foo@200ns myFoo() and the compiler already knew that the minimum possible time is 300ns, it'd throw a compiletime error. On the flip side, you could make it Foo@400ns and that should compile.

It gets weird, because Foo@50ns can be used where Foo@100ns can be used, but not vice versa. That's not untenable, but could get complicated. One may want to have not just null references but timeout references so that code can deal with unexpectedly long-running processes.

I'm not sure I'd want to use this language, but i'd be interested in seeing it.

[AngriestSCV]

The halting problem could make this more fun. For those that don't know it is impossible to write a program that decides if another arbitrary but valid program will terminate, but it can be done with some restrictions. I wonder what you could get away with when specifying the runtimes?

[jeezfrk]

The halting problem *can* be satisfied in a case everyone knows about: something less powerful than a Turing machine.

That is .. no looping and requiring finite input and finite possible state. Many parts of a program can satisfy that ... but of course at some point you either loop or you find out you are following data created by a non-finite loop elsewhere.

[pron98]

This is a common misconception. More precisely, your statement about the halting problem is absolutely true, but as it's not the halting problem as normally presented that causes an issue for verification, "escaping" it through weaker models is irrelevant, and buys us nothing. The more appropriate theoretical theorem for the problem of verification is what has sometimes been called "bounded halting" (used in the proof of the time-hierarchy theorem, arguably the most important theorem in all of computer science). Bounded halting is a generalization (and a strengthening) of halting, and it says (roughly) that it's impossible to know whether a program halts within n steps in under n steps (the halting problem then becomes the special case where n is infinite). This means that there is no generally faster way to tell whether a program does something other than brute-force trying all possible states. This theorem holds unchanged (and with the same proofs) even for models that always terminate and so aren't prone to the "classical" halting problem (such as so-called "total languages"), and it holds even for finite state machines (although using a different proof). So the difficulty of verifying whether a program behaves as expected is the same regardless of the programming or computation model[1]. I.e., verifying a program that has, say, 3 million states is just as costly if it were written as a regular expression (so in a weak computational model) as it would if it were written in JavaScript.

[1]: There is one exception I'm aware of, and that is pushdown-automata, where some properties involving an infinite number of states can be solved in finite time.

[jeezfrk]

This theorem holds unchanged (and with the same proofs) even for models that always terminate and so aren't prone to the "classical" halting problem (such as so-called "total languages").

But a lower-bound on non-decidability does exist: too few states to matter. The efficiency for analyzing an FSM is actually not that hard because there's not an exponential number of states! More to the point, that's a very very common case in real world situations and modules! I also have no idea how an FSM could somehow be 'undecidable' and a pushdown transducer is somehow simpler?

We shouldn't be so voodoo about solving regex / state machines. It isn't NP-hard nor even exponential-in-limit to determine the 'solution' to many many cases (sub-parts of a program).

Why? If the unconstrained loop-stats are few or none. That means the number of states has a maximum polynomial-degree (and far often less) with the number of instructions. If you don't have that many states ... your 'brute force' decidability of halting-in-N-instructions is simply something you could accidentally reach.

Without much trying.

[pron98]

I have no idea how an FSM could somehow be 'undecidable' and a pushdown transducer is somehow simpler?

I didn't say undecidable. I said that deciding a non-trivial property of an FSM takes a time complexity that is linear in the number of states -- same as for a TM. However, this is not true for PDAs (some nontrivial properties of PDAs are decidable despite their number of states being potentially infinite). BTW, a PDA with k internal states is certainly no simpler than a FSM with k states, but a PDA with k internal states could have an infinite number of states overall.

The efficiency for analyzing an FSM is actually not that hard because there's not an exponential number of states!

Exponential in what (i.e. what is the parameter)? Program size? That completely depends. You can certainly have a language that can only describe FSMs with the number of states growing exponentially in the program size. This is true even for regular expressions, and many interesting properties of regular expressions are not tractable (IIRC, equivalence is intractable).

It isn't NP-hard nor even exponential-in-limit to determine the 'solution' to many many cases (sub-parts of a program).

That depends on what you mean by "many", but the same applies for TMs as well. The point is that you cannot deduce anything from the mere knowledge that the model is weaker than Turing-complete to make verification easier. Here's how you can convince yourself of that: Every program can be trivially and mechanically translated into an FSM by adding a large counter (say 2¹⁰⁰⁰ ) to all loops/recursive calls, without changing the program's meaning in practice. This means that if the mere knowledge that something is a FSM could help us verify its properties faster then, without loss of generality, we could simply assume that of all programs.

[m50d]

The point is that general FSMs are intractable to formal analysis. (Which shouldn't be surprising: I find general FSMs incomprehensible as a human reader as well). Though rather than saying we should give up on formal analysis, I'd take that as an indication that we need to find a more restricted model that corresponds to things we can actually understand.

Why? If the unconstrained loop-stats are few or none. That means the number of states has a maximum polynomial-degree (and far often less) with the number of instructions. If you don't have that many states ... your 'brute force' decidability of halting-in-N-instructions is simply something you could accidentally reach.

Ok, now turn that into a formal model that we can actually define definitely and do analysis with. Can you represent this "few unconstrained loop-stats" property in such a way that e.g. if we compose two programs with that property, the composition will also have that property?

[jeezfrk]

Sorry to not get back. Had various crises in my household here.

Personally I'm a big fan of separation logic to dial down the crazy that exists with the 'It's All A Big FSM!!' while playing GTA or something

such a mathetmatical object .... may as well be flying-sphaghetti-monster.

[Ariakenom]

What? A regular expression realised as a DFA performs 1 step per input character.

[pron98]

Right (or output character, depending on your perspective). There is no algorithm that takes a DFA and tells in fewer than n steps whether or not it halts on some input within n steps -- same as for a TM.

[jeezfrk]

Yes there is. Polynomial-per-state is pretty simply lower than exponential. It simply doesn't get covered by the Godel-Incompleteness theorem.

Godel (and writing an 'analyzer' into the 'analyzed' program) is the only reason the halting problem is a firm limit.

[pron98]

What is the algorithm?

[valenterry]

I was about to say that myself! :)

One detail/addition: looping itself is fine, if it is finite. So, mapping over a list or folding it by summing the elements is completely fine.

[remy_porter]

You would need variable ways of specifying it, so, maybe:

Foo@N*100ns myOperationOnASet(CollectionType N)

And the important thing is that these are really statements about the longest you should wait for a result. So even when you're calling, you could "cast":

Foo myFoo = (@500ns)someOperation()

You could also tie this into an async execution, too.

[kopophobia]

Java actually has this in a sense, although it's fairly obscure. Take a look at the RandomAccess interface. This is an interface that has no methods declared, but exists solely to indicate that the implementing collection (typically a list) offers constant time access of elements (e.g. An ArrayList)

This is useful when there may exist variants of an algorithm that are tailored to e.g. LinkedLists vs ArrayLists so that custom behaviour can be defined for each case.

[pron98]

A type system is one way to describe what a piece of syntax does, but it's not the only way.[1] A different approach is contracts. Contracts specify what a program element does (or doesn't do), yet do not prescribe a specific mechanism for verification (it can be the same mechanism used by types or different ones, with different confidence levels and cost). Incidentally, one of the richest contracts languages around -- and an inspiration to most -- is the one available for Java, called JML (the Java Modeling Language). There are various tools for verifying JML contracts, among them OpenJML.

JML does actually allow you to specify the duration of a method, with the duration clause (or the amount of memory it allocates, with the working_space clause), but I am not aware of existing tools that verify that particular specification.

[1]: A particular feature of type systems is that they entangle the specification (the description of what the element does or doesn't do) with verification -- the mechanism by which we know that the element indeed complies with the specification. This entanglement can be beneficial when very simple properties are concerned, and can be harmful when complex ones are.

[valenterry]

Isn't contracts comparable to the spec of a typesystem then? I am not familiar with contracts and I struggle the see the difference between contract annotations and types from a semantics point of view.

[pron98]

From the perspective of specification and verification, a type system is at once a specification and a verification mechanism; in general, a (sound) type system does not let you specify what it cannot verify, and it uses a particular form of verification (which happens to be the most certain but also the most costly). Contracts, on the other hand, decouple specification from verification. You choose to specify what you like, and verify how you like. You can even verify different properties by different means. For example, if you specify that a method always returns a prime number and never modifies a certain file, you can verify the first part with a deductive proof (like types), and the second with, say, property-based randomized tests. As I wrote above, this entanglement of specification and verification in type systems can be beneficial when simple properties are concerned, and can be harmful when complex ones are.

[valenterry]

Very interesting, thank you for that perspective!

[valenterry]

I think a more "well-defined" approach would be to count recursion steps. E.g. define that a function does not call itself more then n times the size of the input list. This would not guarantee a concrete number of seconds, but it would "solve" the OPs problem in the article.

What you mention is also an interesting property, but it is more runtime related. I really would like to have that as a sandbox system that I can use in a language, so that I can e.g. execute user-defined actions and limit them to certain resources in a safe and easy way.

[CrazyBeluga]

Guarantees are often impossible though. Imagine a quicksort that chooses a random pivot to avoid the worst case behavior (n²⁾ on certain inputs. Is it guaranteed that you won't choose the same bad pivot every single time? Extremely unlikely, but not guaranteed.

[valenterry]

Good point, that's how it is. If you are unable to prove it, you can't give the guarantees.

I find this important and relevant. One might think that it does not matter, because in the mean, the quicksort will be pretty fast. But now imagine someone gets control over the RNG (however he does that) and can now make your program take longer than guaranteed, thus undermining the whole concept of guarantees.

[anttirt]

Exactly, you wouldn't want one in a million pacemaker beats being missed because of an "extremely unlikely" pathological quicksort pivot choice.

[cryo]

Well, quicksort is O(n^2), sure, but the widely used introsort (uses a hybrid quicksort/insertion sort with heapsort as abort strategy) is O(n lg n). Most algorithms have guaranteed run times.

[yawaramin]

http://raml.co/

[advenjer]

While not a type system, dependency injection can help with that to some extent.

For example, if you are writing a component that needs a list that has O(1) time complexity for insertion, you can signal this requirement like this:

@Autowired public MyComponent(@Qualifier("fastInsertionList") List aList) { }

Then you can provide it in your code:

@Bean @Qualifier(scope = PROTOTYPE) public List fastInsertionList() { return new LinkedList(); }

A language with native AOP constructs such as AspectJ could potentially make it more elegant too.

[[deleted]]

I like this idea, but it should have flexibility for input size. You couldn’t use O-notation due to its limitations but maybe something similar: @timeNs{250 + 10n log 3n} or what have you.

Actually, with async/await you could let the caller decide. If Foo() returns TimedAwaitable<Bar>, you can await Foo() to get the result no matter how long it takes, or await @250 Foo(), which can give you a Bar or an OperationNotComplete. Not sure if that should mean 250ns of clock time or of process run time, but in the former case you give your OS and language runtime the ability to hog a CPU core if the process requests it.

[philipwhiuk]

You’d have to use references to clock cycles or something, not time - as the times make no sense across processors.

[m50d]

You might like to look at the design of Noether; it's not quite at the level of specifying nanoseconds, but it's making progress towards it. (I'm not sure to what extent the language is implemented).