Re: Is Smart Eiffel ready for large-scale application ?

On Sun, Apr 17, 2005 at 01:01:36AM +0100, Joseph Kiniry wrote:
> Hi Hendrik,
> 
> On 13 Apr, 2005, at 15:22, Hendrik Boom wrote:
> 
> >On Tue, Apr 12, 2005 at 11:01:08PM +0100, Joseph Kiniry wrote:
> >>Are you working as part of a research team, or are you working on 
> >>these
> >>(very lofty) goals on your own.
> >>
> >>Joe
> >
> >Mostly on my own.  I have some collaborators, but they provide moral
> >support and advice rather than components.  They seem more interested
> >in using the completed system (if and when) for secure networked
> >distributed computing.  For me it's a long-term thing.  I find
> >myself returning to it whenever more immediately useful things allow.
> 
> There are a number of groups around the world doing research in this 
> domain; perhaps you should collaborate with them?

I'm aware of some of them.  I'm a member of IFIP WG 2.1, which is working
on issues relating to program transformation and algorithmic language.
But that doesn't help with the grunt work of programming large systems.
And for reasons of health, I haven't been able to travel to recent meetings.

> 
> >I want to accomplish a proof of concept.  Once it works and is found 
> >useful,
> >it will always be possible to find energy to improve it.
> 
> Most folks think that such a system requires several man-years of 
> effort.

For a complete and usable system, yes.

> Collaboration is key to getting anything done, in my opinion.

Are you offering? :-)  

But first I would need to establish a framework system that has
enough structure and is enough like a complete one that
collaborators can understand what to contribute.  And it would
have to be functional enough that they can see the point in
doing so.

My approach is a little esoteric -- 

I've noticed several things
  -- the most widespread form of verification we have today
	is strong type checking (althoug it doesn't verify everything
	one might need, it's extremely useful)
  -- types can be massively generalised to a full-fledged logic
One possible next step would seem to be to design a programming
language whose types bear a close resemblance to constructive type theory.

About twenty years ago, I took that step, and managed to write a program
that sorted a list, and whose type expressed that the resulting list had
same elements as the argument and was also sorted.

Unfortunately, type-checking it took about twenty minutes of processor
time.

Well, machines are a lot faster now, and programming tools are better,
so I decided to have another look at this problem.  I expect to be able
to reimplement a new type-checker with not too much trouble
(after all, I know what to do now), and have some fun with it.

As for running programs, well that's another project.  That's the one
for which I wish I had a compile-into-memory code generator with
a suitably free licence.  And that's the one on which I would like
some help.  It would be really nice to be able to acquire, verify,
transform, compile, and run programs in full security.  Perhaps as
part of a browser or a public CPU server.  But *that* is yet another
project.

-- hendrik

> 
> Joe
> ---
> Joseph R. Kiniry
> Dept. of Computer Science, University College Dublin
> http://secure.ucd.ie/
>