[bitc-dev] Application vs. Systems programming

[Jonathan S. Shapiro]

On Sat, 2006-02-18 at 02:43 +0000, David Hopwood wrote:

> > But BitC is intended to be a verifiable system development language.
> 
> Why is there any contradiction here? These features do not make programs
> any more difficult to verify:
> 
>  - Varargs can have a trivial interpretation, for example if argument
>    "lists" are real (cons) lists.

If they are "real" (cons) lists, then we are done talking about systems
languages. Cons cells are a reference type. The problem here is that you
are going to need dynamic type to deal with this, and we aren't going to
go there in BitC.

>  - Tuples and pattern matching effectively provide multiple return values
>    without need for an explicit feature.

This is very weird -- I said something similar in email around noon, but
it looks like it didn't make it out to the list. Oh well.

>  - Tail call optimization is an optimization; requiring support for it
>    doesn't affect semantics.

Yes, it does. It makes the difference between knowing that your program
executes in bounded memory or not. Since this alters the exception
behavior it is a semantics issue.

The current "relaxed" tail call requirement in section 10.1 of the
specification covers the overwhelming majority of tail call uses
observed in the wild.

shap