Is there a technique for statically checking that a function is only called at a particular rate?

I was reading this article about types, and started wondering how static type checkers could enforce other properties in programs. For example, say I wanted to create a language which would allow checking at compile time that a particular function was only called at most once every 300ms. How would I go about specifying the language to allow that to be enforced? What existing languages try to enforce similar properties?

The property you mention is probably not something that sounds like an ideal fit for enforcement by type systems, so it's not the first example I would suggest looking at, if you want to learn more about how type systems can be used to enforce a variety of properties. (I'm not saying it is impossible to enforce that property using a type system, but it might not look natural or feel super-useful to an everyday programmer, and the type system might need some hand-holding or help from the programmer.)

However, there are other properties that are a better fit for type systems. For instance, you might look at dependent type systems, which can be used to enforce many properties.

In my experience, type systems tend to be more useful for enforcing safety properties. It tends to be harder to reason about time or liveness properties using a type system (I'm not saying it is impossible, but it might be harder or less natural).

You might also enjoy reading about the Curry-Howard correspondence, which shows a correspondence between theorems and types (and between a proof of a particular theorem vs a particular program that can be given a particular type). Proof-carrying code is one example of a system that relies heavily on this view of proofs-as-programs. The goal there is to prove non-trivial properties of a program. The theorem you want to prove gets encoded as a type, and the proof gets encoded as an expression in an abstract language; then checking the validity of the proof becomes as simple as checking that the expression has the claimed type. This essentially shows how you can reduce "showing that the program satisfies a particular safety property" to type-checking.

In a similar but not identical vein, you might also enjoy looking at languages like Haskell and the QuickCheck tool, which uses the rich type information available from the Haskell type system to synthesize test cases. Anecdotally, QuickCheck is effective at finding many bugs. This is not an example of using the type system to enforce absence of a particular kind of bug, so much as using the type system to make random testing more effective and thereby tend to help programmers catch many bugs earlier.

StackExchange Computer Science Q#30714, answer score: 4