# Correctness-checking, type-checking, stack effects, constraints, etc.

## cpcogan — 2004-12-30 22:31:51

    Can we analyze for correctness? In general, no.

    But the range of programs that we can analyze for correctness by

    mechanical means is not just "toy" programs.

    By constraining the development tools in certain ways, we can make

    programs that are both powerful and yet mechanically verifiable in a

    reasonable time by software.

    I don't mean that we can test for correctness in the sense of: Does

    it do what we want it to, but rather in the sense of: Is it, as it

    stands, a complete and logically coherent piece of software. This

    means testing that all references are satisfiable, that all

    recursions can end, that each defined component is defined according

    to mathematically-describable rules on the basis of previously-

    defined entities.

    James Martin wrote about this, in _System Design from Provably

    Correct Constructs_ (Prentis-Hall, 1985). The method he describes

    used non-standard control construct equivalents, and started from a

    set of mathematically-defined primaries. The design software was

    graphical (trees) and, after verification, code was generated

    completely mechanically (mechanical generation of source, alone,

    eliminates coding errors).

    All the data available within a control construct equivalent had to

    be explicitly stated, and it had to be explicitly divided into input

    and output (and the same item could never be both an input and an

    output). Each data item was dynamically assigned a value once and

    once only, so they weren't variables in the ordinary sense (though

    the same name could be assigned another variable in a separate

    execution, of course).

    The three basic control construct thingies could be used to define

    more-complex construct thingies, so the method wasn't as restrictive

    as it might seem at first.

    Anyway, the point is that the various restrictions at the

    foundational level led to a method that led to designs that were

    provably correct (in a logical/mathematical sense, not necessarily in

    a correct-for-the-problem sense), and this in turn enabled complete

    code to be generated mechanically.

    The question is: Can we do something similar with Joy or one of the

    other of our various languages? Because of the way we can "package"

    control constructs and such, it would seem that we are well on the

    way towards just such a mechanically-checkable tool. What the method

    described above had that our languages don't is mainly static

    parameter-and-type checking.

    What I'm wondering is: Can we add a mechanism that allows for static

    checking in those cases where we *want* it, without having this same

    mechanism get in our way when we want to do without it?

    One thing that comes to mind is stack marking, and assertions for the

    compiler. The assertions would tell the compiler how many and what

    kinds of paramters are required. Stack marking would enable the

    compiler to tell (in some case) whether there will be the right

    number and types of parameters *for the given function* on the stack.

    If all of our functions have statically-known stack effects, we can

    have large stretches of code where a mechanical checker could work.

    But what of functions that may take different numbers of items off

    the stack and put different numbers of items back? Each time we

    encounter such a function, our static code checker will fail until

    some "clean" point is found later on (or outside of the caller,

    perhaps, if it can be guaranteed to leave the stack in a statically-

    known state).

    Obviously, if we are going to do static checking for such cases, we

    need something "smarter" than just paramter-counting and type-

    checking. We need to have it analyze the code of the function that

    has the "unstatic" behavior and see if *it* is correct. I think this

    can actually be done (perhaps with another constraint or two). After

    all, a function that pushes the integers 0 through N, given N, could

    well be doing something we want, couldn't it? (we could have it

    produce a list with the numbers in it, but the idea here is to do

    correctness checking without restricting our way of handling the

    stack).

    It seems that this should all be possible, if all of the *primitives*

    have fixed stack effects or if the stack effects are at least

    generally describable to the checker.

    I suppose it's possible that this degree of freedom in stack effects

    would produce a combinatorial explosion of the same kind that makes

    the general problem of program correctness effectively unsolvable for

    any but the simplest programs. But, I'm hopeful that this would not

    be the case, or that if it is, we could restrict uncheckability to

    self-contained parts of our applications, so that overall correctness

    could be checked *assuming* the correctness of these uncheckable

    parts.

    Ideas? Comments?

## William Tanksley, Jr — 2004-12-30 23:11:56

    On Thu, 30 Dec 2004 22:31:51 -0000, cpcogan <ccogan@...> wrote:

     > By constraining the development tools in certain ways, we can make

    > programs that are both powerful and yet mechanically verifiable in a

    > reasonable time by software.

     Yes -- SPARK ADA does this sort of thing to Ada. Very impressive, and

    worth a read.

     > What I'm wondering is: Can we add a mechanism that allows for static

    > checking in those cases where we *want* it, without having this same

    > mechanism get in our way when we want to do without it?

     Here's a different question:

    Can we design a language that can be /subsetted/ such that the subset

    is both checkable and useful?

    I think that's a more acheivable goal than designing a language that's

    both safe AND never gets in the way of someone just wanting to hack

    out code.

     > One thing that comes to mind is stack marking, and assertions for the

    > compiler. The assertions would tell the compiler how many and what

    > kinds of paramters are required. Stack marking would enable the

    > compiler to tell (in some case) whether there will be the right

    > number and types of parameters *for the given function* on the stack.

    > If all of our functions have statically-known stack effects, we can

    > have large stretches of code where a mechanical checker could work.

     You've read about strongForth, right? Its website is long gone, but

    the wayback machine has it in its archives.

     > Obviously, if we are going to do static checking for such cases, we

    > need something "smarter" than just paramter-counting and type-

    > checking. We need to have it analyze the code of the function that

    > has the "unstatic" behavior and see if *it* is correct. I think this

    > can actually be done (perhaps with another constraint or two). After

    > all, a function that pushes the integers 0 through N, given N, could

    > well be doing something we want, couldn't it? (we could have it

    > produce a list with the numbers in it, but the idea here is to do

    > correctness checking without restricting our way of handling the

    > stack).

     I can handle limiting iterations to be over arrays, but then we'd have

    to deal with recursions; so your question seems to me to be

    reasonable.

    The theory of structured programming indicates that there should be

    three ways to create variable stack effects: repetition, composition,

    and alternation. "Repetition" refers to the effects of loops; it

    happens when the same known stack effect happens an unknown number of

    times. "Alternation" refers to the effect of conditionals; it happens

    when there are two possible stack effects, only one of which will

    actually happen. "Composition" is when you have multiple different

    stack effects appearing one after the other; it happens in the process

    of normal code and is usually easily handled, but when it appears

    inside of a conditional block of code there must be some way to group

    all of the stack effects together as one side of a conditional stack

    effect.

     > It seems that this should all be possible, if all of the *primitives*

    > have fixed stack effects or if the stack effects are at least

    > generally describable to the checker.

     Recursion makes the first requirement impossible. I believe that being

    able to describe the general effect using terms like the ones I use

    above will solve the problem.

     > I suppose it's possible that this degree of freedom in stack effects

    > would produce a combinatorial explosion of the same kind that makes

    > the general problem of program correctness effectively unsolvable for

    > any but the simplest programs. But, I'm hopeful that this would not

    > be the case, or that if it is, we could restrict uncheckability to

    > self-contained parts of our applications, so that overall correctness

    > could be checked *assuming* the correctness of these uncheckable

    > parts.

     I agree that this is extremely possible, and I'd love to see it (I'd

    love to work on it, if I had time).

    -Billy

## Slava Pestov — 2004-12-31 01:40:45

    cpcogan wrote:

     > that all

    > recursions can end,

     This is not possible without using a non turing complete language!

     > (mechanical generation of source, alone,

    > eliminates coding errors).

     But coding errors are easy to fix. Mechanical generation does nothing

    for logic errors.

     > But what of functions that may take different numbers of items off

    > the stack and put different numbers of items back?

     Do such functions matter?

     > It seems that this should all be possible, if all of the *primitives*

    > have fixed stack effects or if the stack effects are at least

    > generally describable to the checker.

     Have you played with Factor? It already does static stack checking. Only

    the stack effects of primitives (170 or so) are entered manually; all

    other stack effects are inferred. More than half of the words in the

    library have a known stack effect.

    Slava

## Philippa Cowderoy — 2004-12-31 03:05:21

    On Thu, 30 Dec 2004, Slava Pestov wrote:

     >

    > cpcogan wrote:

    >> that all

    >> recursions can end,

    >

    > This is not possible without using a non turing complete language!

    >

     However, it's worth asking whether there's a suitably useful subset of

    turing complete available - for many use patterns there is, and certainly

    being able to prove that a given piece of code lies within that subset

    would be useful. Another idea that may prove useful is that some type

    systems with subtyping (System F^ comes to mind) don't actually have a

    notion of type-check failure, the equivalent concept being merely not

    being able to say anything useful about a value ("it's somewhere in the

    set of all possible values including non-termination").

    --

    flippa@...

    Ivanova is always right.

    I will listen to Ivanova.

    I will not ignore Ivanova's recomendations.

    Ivanova is God.

    And, if this ever happens again, Ivanova will personally rip your lungs out!

## William Tanksley, Jr — 2005-01-01 04:29:17

    Philippa Cowderoy <flippa@...> wrote:

     > On Thu, 30 Dec 2004, Slava Pestov wrote:

    > > cpcogan wrote:

    > >> that all

    > >> recursions can end,

    > > This is not possible without using a non turing complete language!

    > However, it's worth asking whether there's a suitably useful subset of

    > turing complete available - for many use patterns there is, and certainly

    > being able to prove that a given piece of code lies within that subset

    > would be useful.

     That's also impossible in general -- but you're right, it's a good

    thing, so the people at http://www.praxis-his.com/sparkada/ did it.

    The trick is that although it's impossible for a Turing machine, it's

    quite possible for a Turing machine with an oracle; thus, if you have

    the programmer insert a little extra formal stuff into the comments,

    your code can be classified.

    The trick with SPARK Ada was:

    1. Pick a language that was clearly and reasonably unambiguously

    defined. Ada was chosen.

    2. Choose a subset of it that's entirely invariant across all

    platforms according to the specification. The result is called SPARK

    Ada, in this case; some of the things that were NOT included were the

    ability to use side effects in functions, multitasking, and dynamic

    memory allocation.

    3. Define a set of mandatory annotations that fit within comments and

    allow the SPARK compiler to perform certain architectural analyses.

    4. Design a set of proof annotations -- including preconditions,

    postconditions, and so on -- that allow the SPARK theorem prover to

    analyse the code for various conditions. Analyses may include maximum

    stack depth, total exception freedom, total runtime freedom (there are

    now Ada compilers that will generate a no-runtime-required image), and

    so on.

     > flippa@...

     -Billy