On 09/03/14 00:40, Mike Gran wrote: > On Saturday, March 8, 2014 12:57 PM, Mateusz Kowalczyk > <fuuze...@fuuzetsu.co.uk> 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.
