[bitc-dev] BitC surface syntax, theorem proving

[Sandro]

On the topic of combining programming with theorem proving, I'm not sure if this was brought up yet:

"Combining Theorem Proving and Programming"

http://www.cs.bu.edu/~hwxi/academic/papers/icfp05.pdf

It describes how the Applied Type System, expressed in a
dependently-typed language (http://www.cs.bu.edu/~hwxi/ATS/ATS.html),
supports theorem proving.

ATS also supports safe, fully typed imperitive programming with pointers, which may be relevant to proving properties of many BitC programs.

Ah, I  see Swaroop already pointed it out before:

http://www.eros-os.org/pipermail/bitc-dev/2005-July/000254.html

The paper may still be of interest if it hasn't already been seen.

Sandro

----------------------------------------
From: "Jonathan S. Shapiro" <shap at eros-os.org>
Sent: Monday, August 07, 2006 6:06 PM
To: BitC-Dev <bitc-dev at coyotos.org>
Subject: SPAM-LOW:  [bitc-dev] BitC surface syntax 

Many of you have said, in various forms:

	LISP syntax really sucks.

In fact, it has been suggested that "LISP" originally stood for "Loony
Idiots Stick to Parenthesis". :-)

A recent conversation with Mark Miller has convinced me that we may be
able to drop this syntax.

  [Long pause to wait for applause. Remember that the Europeans won't
   see this until tomorrow AM, so we need a *very* long pause. :-)

   In fact, I have just heard the distinctive sound of a certain
   anonymous reader down at a certain anonymous Defense think tank
   falling out of his chair. ]

The original reason for using s-expression language was the need for
quasiliteral patterns. We had a very bad experience with quoting and
quasiliteral issues in HOL, which led me to say to myself "I don't want
to think about quoting issues while I'm wrestling with language design,
so let me put this issue off." Since it was a solved problem in the LISP
family of languages, I adopted a LISP syntax (over many objections).

[...]

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.coyotos.org/pipermail/bitc-dev/attachments/20060814/aff1990a/attachment.html