Re: Writing libraries for C programs using Guile Scheme

[Mateusz Kowalczyk]

On 09/03/14 00:40, Mike Gran wrote:
> On Saturday, March 8, 2014 12:57 PM, Mateusz Kowalczyk <address@hidden> wrote:
>
>
>> I'm asking how the perfect setup is going to be achieved. Simply writing
>> the library in Guile does not make it secure (or maintainable for that
>> matter). My sole question to the opening post is ‘how will the library
>> be assured to be secure?’. That is all I wish to know from this thread.
>
>
> Pardon in advance this slightly OT aside...
>
> Back in the day, I used to do safety critical software for a living,
> mostly using standards built up around RTCA DO-178B.  All quite formal
> stuff, and very legalistic, and focussed on embedded avionics systems.
>
>
> Guile would never pass muster for DO-178B or C. But, the one way in which
> Scheme is quite compliant is -- if you avoid call/cc --it is fairly easy,
> to enumerate the number of entry points, exit points, and branches in a
> given procedure.  The complexity of a program can be computed and
> bounded.

Great, an answer! Is there anything in place which lets you do this
already? While it does sound nice I imagine that it'd be difficult to
implement. I'm interested in any reading you can recommend because I
managed to find very little about proving/assuring correctness of
LISP/Scheme programs.

> This is could be said of any program written in purely functional style,
> I suppose.  So that's an advantage with respect to security.

Guile is not purely functional. You can try really hard to write
programs in such style but I believe there are big performance
problems with such approach in languages without static analysis. Am I
wrong? Is updating an immutable structure (creating a new one and
preserving the old one) as fast as just calling set! ? In compiled
languages the compiler can see where the structures will be used &c
and decide what can be safely mutated in the background and what
can't. I believe that Guile doesn't have such a mechanism in place.

It might of course be a non-issue from the performance aspect. I
simply worry about how functional purity is going to be enforced if
this approach is taken.

It's a bit like trying to write purely functional programs in (a subset
of) Java.
Sure, it's possible, as long as you don't use anything out of the
standard library (or any other library) and very strictly adhere to
certain restrictions. I read a paper couple of months/years ago about
a subset of Java that could be considered purely functional.
Unfortunately, I can't locate the paper anymore but I can assure you
that _a lot_ of stuff had to be thrown out of the window.

I guess my question here is: is it viable to write non-trivial purely
functional programs in Guile? (Is the performance OK? Can we assure
that something is purely functional somehow?).


>>> But the bit's needs to be in place. Why don't we try to copy
>
>>> typed racket over to guile?
>>
>> Unfortunately Typed Racket is truly horrible to write, read and use. I
>> think it is a prime example of what happens if you try to tack on a
>> simple type system on top of an existing LISP/Scheme dialect. Personally
>> I think the time spent implementing such abomination would be better
>> spent be triple-checking code in Guile as it is today. It is just an
>> opinion and you're free to disagree of course.
>
>
> Scheme itself is pretty horrible to read (but fun to write and use).  How
> much worse could it be?

This is pretty much exactly what I was thinking when I sat down to try
out Typed Racket and today I can say ‘much worse’.

> But if software safety is your goal, I'd go with ADA.

Personally I like Agda but each to their own. Unfortunately I think
writing the library in another language all together is not an option
here ;)

> Un-seriously yours,
>
> Mike Gran
>


--
Mateusz K.