[plt-dev] #lang: the stake in Dracula's heart?

On Mon, Feb 1, 2010 at 2:26 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
> Can't the language come with code that makes the
>
>  #lang acl2
>
> line appear and disappear on write/read from the program's file?
>
> As for sending it from drscheme to the ACL2 theorem prover, I
> imagine that this is all under your control. -- Matthias

DrScheme needs to be able to read ACL2 files written by other
programs, such as the ACL2 books.  ACL2 should be able to read files
written by DrScheme directly, without always having to go through
Dracula.

If we want ACL2 to "open up" for compatibility with other tools such
as Dracula, there's a quid pro quo that we not make our own tool
needlessly incompatible with ACL2.

--Carl