Lambda the Ultimate

andrew cooke: ...they have type inference with optional annotation like (+ a b) : int, which immediately raises at least two questions: (1) how do you represet that as BitC data and (2) what's the point of having code as data if you have a static type system anyway (i'm assuming BitC hasn't got some amazingly cool typed macro or meta facility)?

Well, if the type annotation is optional, then the representation reduces to S-expressions, and now we're just talking about a Lisp with type inference, a la Stalin, CMU CL, and/or SBCL.

As for code-as-data in the presence of static typing, it's still quite useful; see MetaOCaml for example, or take note of Objective Caml and camlp4. Perhaps the best example of the practicality of it that I can think of offhand is still Graydon Hoare's One Day Compilers presentation.

i thought the lisp-with-inference implementations did inference where they could, and ignored the rest, leaving it to runtime. as far as i know they don't include static analysis of macros (a la metaml, which i'm aware of) because it's still considered quite a hard problem (which is why i also think, as i said, that it's not in bitc). and since they cite ml as an influence on the language i'm assuming bitc is completely statically checked which, with the assumption above, implies that it doesn't have macros (the word "macro" doesn't appear in the document).

however, then i don't see the point for code as data, hence my question. this appears to be a language without macros which cannot express all source code as data - so why bother with expressing source code as data at all?

looking again at the document, section 11 seems interesting, and may be relevant (but is rather brief).

oh, looking again, i missed this (right at the start) - While the current language specification uses a Scheme-like concrete syntax, this choice is a matter of convenience only. It is entirely possible to build a C-like concrete syntax for BitC, and at some point it may become compelling to do so. - which i guess answers my question. there's no point for the syntax at all. it's just aesthetic [edit - or for making tools/parsing easier, i guess; further edit - or simplifies specifying proofs?].

andrew cooke: ...there's no point for the syntax at all. it's just aesthetic [edit - or for making tools/parsing easier, i guess; further edit - or simplifies specifying proofs?

Certainly to make parsing and macros trivial (well, almost trivial; if they choose to implement hygenic macros a la R5RS there's some hair there). You're probably right about representation for proof-checking also, though, as they reference the ACL2 theorem prover, which is in Common Lisp.

I also note that they say of adopting a C-style syntax that "it may become compelling to do so." So presumably when stacking the Lisp-style syntax against the C-style syntax they found something compelling about the Lisp-style syntax. Whether that's pure familiarty or some other set of features would be a matter of pure conjecture on my part.

Finally, I have to confess my feeling that their use of Lisp-style syntax, if it is intended to "play nicely" with a theorem prover written in Lisp, may come back to haunt them: it seems to me like it would be wayyyyyyyyyyyy too easy to make errors of confusion between the meta language and object language that way.

Jonathan S. Shapiro

A previous Lambda discussion looks at the issue of statically typed metaprogramming.

See Goubalt-Larreq, Logical Foundations of eval/quote Mechanisms, and the Modal Logic S4.

At the moment, all of the non-sexpr forms in BitC can be canonicalized to s-expr forms. The BitC expression e:T can equivalently be written as

(type-qualify e T)

Actually, we're considering removing the duplication at some point, and if we do we will probably eliminate TYPE-QUALIFY.

A key rationale for the use of S-Expr's in LISP was the desire to program directly in the AST, and the implicit assumption that child positions in AST's should be dynamically typed. This was a reasonable call for a dynamically typed language, but in a statically typed language the role of the "type" is actually very different from the role of the remaining AST children. If you are building an AST for a statically typed language, and you are not being driven by a desire for a macro mechanism (and perhaps even if you are), then it makes sense for AST's to have a distinguished type field and for this to be syntactically distinguished in the source form.

Jonathan S. Shapiro

While we flirted briefly with a macro mechanism, we quickly concluded that it didn't suit our design goals. Any extensive use of macros is intrinsically incompatible with human-transparent program inspection. Since BitC is targeted at critical systems, keeping the code transparent is important to us.

The reason that we want a surface syntax that is close to the AST format has to do with the relationship between BitC/P and BitC/L. BitC/P is the programming language. BitC/L is the logic language. It is extremely useful to be able to write program fragments that are *data* in the eyes of BitC/L. Further, it's very useful to be able to write AST's that have unbound positions (expressed as AST meta-variables). So: the reason we want an AST-like surface syntax is to let us write such program fragments.

Finally, let me just point out that there is no syntactic problem introduced by our deviations from s-exprs. The two forms:

`e:t
`e

are equally parsable.

Jonathan S. Shapiro

Believe instead in the importance of educating yourself in basic concepts which apply to all programming. Learn about the terminology so that you don't misinterpret phrases like "proven correct", which seems to be the basis for your question.

The only way you can ever prove anything correct is with respect to a formal specification. If you have such a specification, then in principle, you may be able to prove that a particular program implements it. Typical compilers perform proofs about the type schemes in programs they compile, for example. In languages with good type systems, these proofs are rigorous and complete, and guarantee a great deal about the runtime behavior of the program.

In the case of BitC, formal specifications are given in the form of assertions (BitC calls them "theorems") embedded in the program source. BitC will attempt to statically ensure, i.e. prove, that these assertions always hold true, or else it will report failure.

To answer the original question a bit more directly, obviously there's no programming paradigm that prevents all algorithmic bugs. However, there are large classes of bugs which can be automatically prevented from occurring. The functional languages tend to have implemented these techniques better than mainstream languages, and in fact mainstream languages have adopted some of these techniques from the functional/academic world. The canonical example is automatic garbage collection, which was invented for Lisp.

A major area of weakness for imperative languages is their very imperativeness. Mutable state leads to various kinds of bugs that cannot occur when mutation is avoided (that doesn't mean you can't use it under controlled circumstances). In general, mutation leads to programs which are harder to reason about, and therefore harder to get correct. If you don't understand why this is the case, or don't believe it, I'd recommend studying HTDP, CTM, or SICP (all mentioned here previously and easily googleable). Perhaps someone can summarize the issues in a few sentences, but the problem with such explanations is that they're incomplete and only really make sense once you've made the effort to learn the details.

Mutation is especially problematic when concurrency is involved. Better models of concurrency than multithreaded shared memory access are not necessarily just a "functional" feature - that's not the point. The point is that better methods exist, and that there are languages which implement them, but the imperative languages currently do not.

Concepts like type inference, pattern matching, closures, continuations etc can easily be properties of imperative languages, too.

That's all true, although imperative languages don't do a very good job of implementing all these things today, which is why they come in for criticism in these areas. In particular, most of them still have major problems with tail calls and recursion, which is a serious constraint on the use of many of the other features. But you could fix all of that, in theory, and you'd still be left with the problem of mutation that's not properly controlled. A "good" imperative language would need to impose proper controls on mutation. In fact, languages like C++ and Java go some way towards this, e.g. with 'const' declarations which can apply to functions, pointers/references, and methods. However, experience with the functional languages shows that they could do a lot better.

I am not a 'script kiddie', nor a newcomer in the computer programming field. I have good knowledge of quite a few languages, and a personal hobby of investigating new concepts and new languages as a way to expand my knowledge on programming.

The only way you can ever prove anything correct is with respect to a formal specification. If you have such a specification, then in principle, you may be able to prove that a particular program implements it.

So all we need to prove all our programs are correct is to have a specification that the PL can verify against. Sounds like bugs are the result of a specification problem, not a programming language problem. :-)

Going back to the topic, on imperative languages you need some mechanism to assert things like:

void updateBar(Foo foo, Bar newBar) {
    foo.bar = newBar;
}

spec updateBar(Foo foo, Bar newBar) {
    ensures(foo.bar = newBar);
    ensures(foo.baz = old(foo.baz));
    ensures(foo.blah = old(foo.blah));
    ensures(foo.foobar = old(foo.foobar));
// ad-nauseum
}

In Eiffel they say this: you should write down how every command (i.e. side-effecting procedure) changes every basic query (i.e. side-effect free function from which the other queries are based on). There are other approaches (e.g. Z) which you can assert which fields change and which stay the same.



It's just the dual of referential transparency: in (pure) FP every function is pure unless declared so, while on IP every function isn't pure unless stated so. FP has (IMHO, YMMV, AFAICT, etc.) more proven techniques to deal with side-effects (e.g. monads, unique types) than IP WRT pure functions (e.g. const in C++ is broken, DbC in Eiffel doesn't cover mutation).



Separating effectful from pure functions/ADTs is a real-world problem (sometimes called immutable/value objects) strongly related to parameter aliasing, race-conditions, equality vs. identity, cloning vs. deep-cloning, etc.. So you can either use programming discipline, exaustive testing, formal proofs, etc. to avoid these issues or let the compiler point the bugs in your program (e.g. using a IORef Int in a context expecting a plain Int). Once you have this you can emulate other features (e.g. "const" modifiers for references) in libraries instead of having to wait language changes.

If you have such a specification, then in principle, you may be able to prove that a particular program implements it.

And as Anton says, In languages with good type systems, [compilers] guarantee a great deal about the runtime behavior of the program. So it seems a shame that (arbitrarily choosing a language I'm familiar with) the type of every Haskell program is bare bones IO (). A program with a more sophisticated type would have guarantees on its front cover, that wouldn't require internal analysis to appreciate. Is there any prospect of applying the good type systems to the interaction between a program as a whole and its system environment?

Is there any prospect of applying the good type systems to the interaction between a program as a whole and its system environment?

Another relevant term is "computability logic".

I am positive we mentioned both of these topics on LtU.

[on edit: then again, there exists An Algebra of Behavioural Types]

Within a Haskell or ML program, types are quite effective. Large pieces such as modules have types, and this is considered useful even though they are far from complete descriptions of the modules' behavior. What's on my mind is not the big problem.

What about using a little type to describe a program's interaction? If a program's output is XML, why not have that in the type of main?

Maybe that's a bad example of a "little type", since XML is a large spec. Would an OS that enforces types be pleasant to use? Could distinct systems agree on type names? That's enough thinking out loud.

it doesn't. who said it does?

I'm going to take a different approach from the other respondents and say that a functional approach DOES help the programmer avoid algorithmic bugs, not by preventing them, but by bringing the structure of the algorithm to the fore.

My own experience was certainly that learning FP got me out of the "state twiddler" mindset of imperative programming, and made me a better programmer even when not using an FP language.

axilmar: I have a sincere question and I would like a sincere answer.

That's certainly fair, and I see that you've gotten several. Let's see if I can support them and perhaps add something new.

axilmar: How does BitC (or any functional language, for that matter) keep the programmer from introducing algorithmic bugs?

Short answer: it doesn't.

Long answer: Richer type systems than are generally found in popular languages tend to be associated with functional languages such as the ML family, Haskell, Clean... with the exceptions, of course, being the latently-typed functional languages such as the Lisp family or Oz. At some level of expressiveness in the type system, things that might be part of an "algorithmic error" can be caught by the type system, by which I mean "at compile time." Having said that, some aspect of algorithmic correctness will always be dynamic, otherwise your compiler wouldn't produce a program; it would just give you the result of the algorithm. In fact, you can observe this phenomenon concretely: just try out any of the implementations of the factorial algorithm as a C++ template metaprogram. So the claim, then, is just that a rich type system prevents a larger class of errors than a weaker type system does.

axilmar: I don't believe in functional programming, as I have worked with it and I haven't found any significant benefits derived from the primary properties of functional programming. Concepts like type inference, pattern matching, closures, continuations etc can easily be properties of imperative languages, too.

Absolutely correct, although in practice they don't tend to be. But I am a big fan of multiparadigm programming as documented and advocated in Concepts, Techniques, and Models of Computer Programming and exemplified in the Mozart-Oz System. You may wish to check it out: it won't prevent you from being imperative if you wish to be, and you may be pleasantly surprised at how uniform the integration of imperative concepts with all the other concepts is.

axilmar: The project I have worked on was a Powerpoint-like application, on Solaris/X-Windows/ML, and it took about a year to develop with two people.

Interesting! I see that the PLT folks have done a functional presentation system in DrScheme: SlideShow. I don't know how many people developed it or how long it took.

axilmar: This question is more important in the context of a programming language like BitC that claims that it is a system's programming language, allowing for implementing operating systems that can be proven correct by the compiler. I really doubt their claims. It also seems strange to me that they say 'it would be necessary to provide a C-like interface'.

I think you're missing a level of indirection here: the compiler doesn't prove the code correct. Instead, the language has a formal semantics that can be codified within a logic implemented by a theorem prover (they've expressed a desire to use ACL2, a very mature theorem prover). They can then use the theorem prover to prove that the encoding of algorithm X in BitC is correct with respect to its specification in the logic that ACL2 implements (is that confusing enough)? This is important for OSes, because getting things like cache coherency, multiprocessor/thread scheduling and prioritization, signal and interrupt handling, etc. right is notoriously difficult, and that's before even considering any of Coyotos' interesting security requirements, which aren't really separable from the other concerns anyway.

With respect to "C-like interface," I don't see that terminology in the spec. Perhaps you're referring to the need to have total control over memory layout, but if so, I can't imagine what would be controversial about that in a language intended to address hardware directly. If you mean the observation that a C-like syntax might become compelling, that would be a purely social/adoption-oriented choice.

axilmar: So please consider this question as sincere.

I most definitely do, all the more so as our backgrounds sound very similar. I was, and still am, a Lisp and Smalltalk aficionado by night and a professional C++ and Java developer by day. I fell strongly on the latently-typed side of that debate for decades, but then discovered type-inference via Standard ML, then Haskell which I've never been able to totally get my brain around, then O'Caml. Dialogue here led me to understand that the action, if you will, was in type theory, and personal friends urged Pierce's Types and Programming Languages on me. Further investigation rapidly revealed how woefully inadequate my understanding of types is and how much progress has been made in the field just over the past few years, with type systems now supporting things like type-safe distributed programming, prevention of race conditions and deadlock in concurrency, enforcing order-of-operation constraints in stateful APIs, enforcing dataflow security constraints, all kinds of things that a naïve concept of types as "descriptions of how bits are laid out" or "lists of operations supported on a value" would suggest aren't possible. I repeat: type theory is where the action is. And I have to apologize for myself if my passion-of-a-convert carries me over the edge at times, as it certainly has in the past. :-)

...type systems now supporting things like type-safe distributed programming, prevention of race conditions and deadlock in concurrency...

I've never heard of this, but find the idea quite intriguing. Are there any good links or papers on the topic that you could recommend?

Me: ...type systems now supporting things like type-safe distributed programming, prevention of race conditions and deadlock in concurrency...

Andrew Kensler: I've never heard of this, but find the idea quite intriguing. Are there any good links or papers on the topic that you could recommend?

Certainly: in type-safe distributed computing I'm referring to Peter Sewell's work on Acute. In type-safe concurrent computing I'm referring to Naoki Kobayashi's work on TyPiCal. Acute was first posted about on this site here, and TyPiCal was first posted about on this site here. It's worth mentioning that one of the example modules in Acute provides the semantics of Nomadic Pict, so once again, there's a connection to the Pi Calculus.

No offense intended towards Paul here, but I think that there is a law similar to Godwin's at work on Lambda: in any discussion, the probability of him mentioning Acute, TyPiCal, and Flow Caml quickly converges to 1

Jeff Cutsinger: No offense intended towards Paul here, but I think that there is a law similar to Godwin's at work on Lambda: in any discussion, the probability of him mentioning Acute, TyPiCal, and Flow Caml quickly converges to 1

No offense taken! I don't deny that when the subject comes to what can be done with static typing, these are particularly suggestive examples of the state of the art, offering features quite a bit more compelling than just "you can perform this operation on this value" or "this is how this value is represented in memory." I like them because, as far as I can tell, any dynamically-typed equivalent can only be approximate: these systems prove the absence of certain undesirable qualities before runtime. Only 100% coverage testing, i.e. another form of type inference, could make the same claim.

...where a bug, in the absense of a formal specification, is a deviation from the programmer (or customer)'s intent. After all, no program (or compiler) can no the intent of a human unless said intent is specified in some formal fashion.

In general, it is a long-established principle that by restricting the degrees of freedom of a design, one improves the ability to reason formally about it. PVR expressed this well in CTM (I can't remember the exact quote, and don't have my copy handy). Functional programming languages (pure ones, that is), by removing side effects, gain the advantage of Referential Transparency, meaning (for the novice) that a term may be freely substituted with its definition without changing the meaning of the term. In imperative languages, a term's meaning may change over time.

Now, many feel that the advantages of losing side effects outweigh the disadvantages. Many others feel otherwise--there is a vocal community that feel the (runtime) mutability of program state (and of the programs and languages themselves!) should be maximized rather than minimized, in order to increase programmer flexibility. Smalltalk and its progeny (Self, Python/Ruby to a lesser extent) emphasize this philosophy. Many of the "typing wars" between the functional and dynamic-OO community (the latter often asserts that static typing and type inference are bad ideas) are a result of this philosophical difference.

Who's right? I don't know, time will tell. What I do know is:

Even if you do have a complete formal specification of a program's requirements, in many cases proving that a program implements that specification is undecideable. Two fallback positions are:

* Accept only programs which are provably correct, reject those which aren't provably correct (which will lead to some correct programs being rejected)

* Reject only programs which are provably incorrect, accept those which might work. Optionally, add runtime checks (assertions, downcasts, bounds checks) to the compiler's output such that incorrect programs will result in controlled failure rather than Undefined behavior.

Again, many people (including many professionals in the discipline) disagree on which approach is better. Many feel it depends on the application--for a flight control system I consider formal proof to be essential, a so-called "CRUD screen" is a different matter.

The difference is that programming in a functional style removes entire classes of mistakes. Functional programs involve no mutatable variables. When you have a variable whose value is changing (in a loop, for instance), it is difficult to ascertain exactly what the possible values of the variable are, especially when you have a lot of "if" statements that set the value.

The functional method is to write a recursive function instead of a while loop. Any new modification of a value must, by definition, be stored in a _new_ variable. This means that you can see the exact method of determining the value of a variable at variable declaration time. You never have to iterate through a loop to determine how a variable gets modified throughout the loop.

This doesn't mean that the programmer can't make basic algorithmic mistakes, but it does mean that the derivation of the value of each variable is clear and easy-to-find. It also makes it easier to prove theorems about functions, since the declarations and definitions are quite clear.

I've got an IBM DeveloperWorks article coming soon about this. You'll see it in about two or three months.

--
Learn to program using Linux assembly language

However, BitC includes a logic language that makes it possible to formally specify what is meant by "bug-free program [fragment]", and it will (as the implementation progresses) include a prover technology that allows many such requirements to be formally demonstrated.

Historically, this type of mechanism hasn't been easy to use, mostly because programmers generally don't know what the intended behavior of their programs actually is. Once you get past that hurdle, you dive into a bunch of verification-related hurdles.

While BitC itself is a general-purpose language, we expect that the prover component will in most cases get used to demonstrate what we think of as "lightweight properties" (the kinds of things you can state in lightweight checkers). In a much narrower and more specialized set of programs (including the Coyotos kernel), we hope that a richer set of correctness invariants will be demonstrable.

The proof will be in the doing.

Jonathan S. Shapiro

...why would you suppose anybody thinks otherwise?

We'll, still being fairly new to functional programming (especially Haskell), I'll tell you why an outsider could think that functional programming cures all of your problems. Because there's a vocal minority of advocates who have adopted as their motto some of the gems below...

• "Once it compiles, it just works!" (and the ever popular "Statically typed programs can't 'go wrong'")
• "I've never had a need to filthy my hands with so crude a device as a debugger".
• "I've never had problems with laziness causing space leaks, I can't believe anyone else could either".

Greg Buchholz: "Once it compiles, it just works!" (and the ever popular "Statically typed programs can't 'go wrong'")

In fairness, it has been more often the case, in my experience, that my O'Caml code "just works" vastly more often than my Java code, and my Java code vastly more often than my C++ code, and my C++ code vastly more often than my C code. The difference between the O'Caml code and Java code, however, is on roughly an order of magnitude closer to "it just works" than my Java code. So it's far from an absolute thing (cf. the question of algorithmic correctness), but I find it totally quantifiable, albeit I've only done so informally.

Having said that, those who say "well-typed programs don't 'go wrong'" either need to admit that they're quoting Milner making a pun ("go wrong" has a specific, well-defined, but not necessarily intuitive meaning in type theory) or learn that they're quoting Milner making a pun. The best brief explanation of the pun that I've seen is in these slides by Martin Abadi.

I agree with what Dominic says about functional programming. I do not agree with his statements about Java verification. The most advanced verification work on Java programs to date has been accomplished on significantly restricted subset languages.

But the thing that BitC is (so far as we knoe, uniquely) trying to accomplish is to allow verification of selected program where explicit control over mutability and representation are required -- such as kernels. This is where the novelty lies.

Having said that, I don't see any reason why we shouldn't be able to do anything ACL2 or Isabelle/HOL or TWELF can do. In our experience, the absence of static types and the limitations of a first-order language were very awkward in ACL2, and the program/logic integration in the HOL-related provers was simply horrible. We're fairly hardcore pragmatists in this regard, and it will surprise me if we do not achieve a more useable integration. Even with better integration, verification is not a simple undertaking.

Our confidence in ACL2 dropped rather a lot when one of my students successfully proved false. We then tried Isabelle/HOL, and learned that the "automated" in "automated theorem prover" is a very relative term. Proving isn't an objective in its own right for us; the objective is high-confidence software. In consequence, we want a much higher degree of automation than Isabelle/HOL provides. We've had good experiences so far using TWELF, and we're currently planning to integrate that prover into the BitC compilation framework.

Jonathan S. Shapiro

Our confidence in ACL2 dropped rather a lot when one of my students successfully proved false.

Oops! You reported this to the ACL2 maintainers, I hope. Can you post the "proof" somewhere?