* Writing libraries for C programs using Guile Scheme
@ 2014-03-07 8:22 Peter TB Brett
2014-03-07 16:30 ` Mateusz Kowalczyk
0 siblings, 1 reply; 11+ messages in thread
From: Peter TB Brett @ 2014-03-07 8:22 UTC (permalink / raw)
To: guile-user
Hi all,
Recently, there have been some really horrible programming errors found in
widely-used and security-critical libraries (GnuTLS, for example).
These libraries are usually written in C because C is a "lowest common
denominator": if a library is written in C, almost every language will be
able to access its functions somehow (for example, in Guile we can use the
dynamic FFI).
I've now realised that it would be *really awesome* to be able to write
some code in Scheme, and automatically generate a .so file (or DLL) and a C
header file that I could then easily (and safely) use in other programs
without any special handling (including via Guile's FFI). I think it would
be much easier to avoid some of these recent stupid "goto fail;" bugs if we
were writing in Scheme.
It seems to me that most of the things needed for this are already in
place, although at some performance cost and probably some restrictions in
the sort of programs that can be written in this way:
- Guile can already pack bytecode into ELF object files.
- Andy Wingo has demonstrated generation of simple native code from Guile
(compost!).
- libguile provides the infrastructure needed to load and run Guile
bytecode, and we can get the dynamic linker to pull it in.
So what's needed? I've had a few ideas for how this could work. Each
function exported by the library needs to have a native code stub in the
ELF .text section, which:
a. Puts the thread into Guile mode
b. Marshals the corresponding Scheme function
c. Deals with uncaught exceptions - probably with SIGABRT.
d. Asserts that the return value from the Scheme function is a pure foreign
type
e. Leaves Guile mode
f. Returns
Unfortunately I'm sure that I've missed some important bits (for example,
thread safety & reentrancy), and I *certainly* don't have enough low-level
Guile knowledge to make this work. So I'd be very interested to hear what
people think about this idea.
Best wishes,
Peter
--
Dr Peter Brett
http://peter-b.co.uk/
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-07 8:22 Writing libraries for C programs using Guile Scheme Peter TB Brett
@ 2014-03-07 16:30 ` Mateusz Kowalczyk
2014-03-07 16:36 ` Mateusz Kowalczyk
2014-03-08 0:32 ` Mark H Weaver
0 siblings, 2 replies; 11+ messages in thread
From: Mateusz Kowalczyk @ 2014-03-07 16:30 UTC (permalink / raw)
To: guile-user
On 07/03/14 08:22, Peter TB Brett wrote:
> Hi all,
>
> Recently, there have been some really horrible programming errors found in
> widely-used and security-critical libraries (GnuTLS, for example).
>
> These libraries are usually written in C because C is a "lowest common
> denominator": if a library is written in C, almost every language will be
> able to access its functions somehow (for example, in Guile we can use the
> dynamic FFI).
>
> I've now realised that it would be *really awesome* to be able to write
> some code in Scheme, and automatically generate a .so file (or DLL) and a C
> header file that I could then easily (and safely) use in other programs
> without any special handling (including via Guile's FFI). I think it would
> be much easier to avoid some of these recent stupid "goto fail;" bugs if we
> were writing in Scheme.
I doubt that going from a single inherently unsafe but bloody fast
language to slightly less unsafe but much slower language is an
advantage here…
>
> It seems to me that most of the things needed for this are already in
> place, although at some performance cost and probably some restrictions in
> the sort of programs that can be written in this way:
>
> - Guile can already pack bytecode into ELF object files.
> - Andy Wingo has demonstrated generation of simple native code from Guile
> (compost!).
> - libguile provides the infrastructure needed to load and run Guile
> bytecode, and we can get the dynamic linker to pull it in.
>
> So what's needed? I've had a few ideas for how this could work. Each
> function exported by the library needs to have a native code stub in the
> ELF .text section, which:
>
> a. Puts the thread into Guile mode
> b. Marshals the corresponding Scheme function
> c. Deals with uncaught exceptions - probably with SIGABRT.
> d. Asserts that the return value from the Scheme function is a pure foreign
> type
> e. Leaves Guile mode
> f. Returns
>
> Unfortunately I'm sure that I've missed some important bits (for example,
> thread safety & reentrancy), and I *certainly* don't have enough low-level
> Guile knowledge to make this work. So I'd be very interested to hear what
> people think about this idea.
>
> Best wishes,
>
> Peter
>
Do you feel like you can provide correctness proofs for your
implementations of such security critical libraries? Scheme isn't
exactly the safest language.
--
Mateusz K.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-07 16:30 ` Mateusz Kowalczyk
@ 2014-03-07 16:36 ` Mateusz Kowalczyk
2014-03-08 0:32 ` Mark H Weaver
1 sibling, 0 replies; 11+ messages in thread
From: Mateusz Kowalczyk @ 2014-03-07 16:36 UTC (permalink / raw)
To: guile-user
On 07/03/14 16:30, Mateusz Kowalczyk wrote:
> On 07/03/14 08:22, Peter TB Brett wrote:
>> Hi all,
>>
>> Recently, there have been some really horrible programming errors found in
>> widely-used and security-critical libraries (GnuTLS, for example).
>>
>> These libraries are usually written in C because C is a "lowest common
>> denominator": if a library is written in C, almost every language will be
>> able to access its functions somehow (for example, in Guile we can use the
>> dynamic FFI).
>>
>> I've now realised that it would be *really awesome* to be able to write
>> some code in Scheme, and automatically generate a .so file (or DLL) and a C
>> header file that I could then easily (and safely) use in other programs
>> without any special handling (including via Guile's FFI). I think it would
>> be much easier to avoid some of these recent stupid "goto fail;" bugs if we
>> were writing in Scheme.
>
> I doubt that going from a single inherently unsafe but bloody fast
> language to slightly less unsafe but much slower language is an
> advantage here…
>
>>
>> It seems to me that most of the things needed for this are already in
>> place, although at some performance cost and probably some restrictions in
>> the sort of programs that can be written in this way:
>>
>> - Guile can already pack bytecode into ELF object files.
>> - Andy Wingo has demonstrated generation of simple native code from Guile
>> (compost!).
>> - libguile provides the infrastructure needed to load and run Guile
>> bytecode, and we can get the dynamic linker to pull it in.
>>
>> So what's needed? I've had a few ideas for how this could work. Each
>> function exported by the library needs to have a native code stub in the
>> ELF .text section, which:
>>
>> a. Puts the thread into Guile mode
>> b. Marshals the corresponding Scheme function
>> c. Deals with uncaught exceptions - probably with SIGABRT.
>> d. Asserts that the return value from the Scheme function is a pure foreign
>> type
>> e. Leaves Guile mode
>> f. Returns
>>
>> Unfortunately I'm sure that I've missed some important bits (for example,
>> thread safety & reentrancy), and I *certainly* don't have enough low-level
>> Guile knowledge to make this work. So I'd be very interested to hear what
>> people think about this idea.
>>
>> Best wishes,
>>
>> Peter
>>
>
> Do you feel like you can provide correctness proofs for your
> implementations of such security critical libraries? Scheme isn't
> exactly the safest language.
>
I should also add that you'd also have to show that the generated object
files reflect the behaviour properly.
I don't mean to sound as negative as I probably am but I'd hate to see a
broken security-critical library which offers nothing but ‘hey we get to
re-write the existing thing in our favourite dialect except slower,
clunkier to use and with new bugs!’.
--
Mateusz K.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-07 16:30 ` Mateusz Kowalczyk
2014-03-07 16:36 ` Mateusz Kowalczyk
@ 2014-03-08 0:32 ` Mark H Weaver
2014-03-08 3:50 ` Mateusz Kowalczyk
1 sibling, 1 reply; 11+ messages in thread
From: Mark H Weaver @ 2014-03-08 0:32 UTC (permalink / raw)
To: Mateusz Kowalczyk; +Cc: guile-user
Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
> I doubt that going from a single inherently unsafe but bloody fast
> language to slightly less unsafe but much slower language is an
> advantage here…
"Slightly less unsafe"? Seriously?
> Do you feel like you can provide correctness proofs for your
> implementations of such security critical libraries? Scheme isn't
> exactly the safest language.
If you'd like to write a new TLS (or other widely-used security
critical) library in Haskell, along with formal and verifiable
correctness proofs, and that would be easy enough to use from programs
written in other languages such that it could actually make a viable
replacement for GnuTLS et al, that would be a great contribution to our
community, and I would *sincerely* thank you for it.
However, what I've mostly seen from you is negativity and FUD about
Scheme and Guile, both here and on IRC. That is _not_ appreciated.
Mark
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-08 0:32 ` Mark H Weaver
@ 2014-03-08 3:50 ` Mateusz Kowalczyk
2014-03-08 16:37 ` Taylan Ulrich Bayırlı/Kammer
0 siblings, 1 reply; 11+ messages in thread
From: Mateusz Kowalczyk @ 2014-03-08 3:50 UTC (permalink / raw)
To: Mark H Weaver; +Cc: guile-user
On 08/03/14 00:32, Mark H Weaver wrote:
> Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
>> I doubt that going from a single inherently unsafe but bloody fast
>> language to slightly less unsafe but much slower language is an
>> advantage here…
>
> "Slightly less unsafe"? Seriously?
Sure. You get rid of pointer arithmetic which is the beg evil in C but
you lose any kind of static typing. It's about as safe as Python, Ruby
and whatever new and hip dynamic language is popular today: not a whole lot.
>
>> Do you feel like you can provide correctness proofs for your
>> implementations of such security critical libraries? Scheme isn't
>> exactly the safest language.
>
> If you'd like to write a new TLS (or other widely-used security
> critical) library in Haskell, along with formal and verifiable
> correctness proofs, and that would be easy enough to use from programs
> written in other languages such that it could actually make a viable
> replacement for GnuTLS et al, that would be a great contribution to our
> community, and I would *sincerely* thank you for it.
I didn't mention Haskell anywhere and neither am I the one posting on
the list saying I'll rewrite these libraries. What I _am_ saying is that
the original poster is considering rewriting security-critical libraries
without stating how the same (and new) bugs are going to be avoided. I'm
simply curious how the security of new libs is going to be assured
because Guile is not exactly a proof assistant where just writing the
program means it's probably correct and you'd be deluded to say otherwise.
> However, what I've mostly seen from you is negativity and FUD about
> Scheme and Guile, both here and on IRC. That is _not_ appreciated.
I don't remember posting any FUD on the lists or IRC about Scheme or
Guile, no matter what I personally think about it. The only things I did
is point out errors or lack of scrutiny over the libraries people
announce sometimes, you being amongst them (and in fact my assumptions
being correct; would you rather have broken libs?). I don't care if you
like me or not but at least don't make shit up. If you have any specific
issues then address them either on IRC or in a separate thread rather
than trying to attack me here.
>
> Mark
>
--
Mateusz K.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-08 3:50 ` Mateusz Kowalczyk
@ 2014-03-08 16:37 ` Taylan Ulrich Bayırlı/Kammer
2014-03-08 16:47 ` Stefan Israelsson Tampe
2014-03-08 20:47 ` Mateusz Kowalczyk
0 siblings, 2 replies; 11+ messages in thread
From: Taylan Ulrich Bayırlı/Kammer @ 2014-03-08 16:37 UTC (permalink / raw)
To: Mateusz Kowalczyk; +Cc: guile-user
Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
> On 08/03/14 00:32, Mark H Weaver wrote:
>> Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
>>> I doubt that going from a single inherently unsafe but bloody fast
>>> language to slightly less unsafe but much slower language is an
>>> advantage here…
>>
>> "Slightly less unsafe"? Seriously?
>
> Sure. You get rid of pointer arithmetic which is the beg evil in C but
> you lose any kind of static typing. It's about as safe as Python, Ruby
> and whatever new and hip dynamic language is popular today: not a
> whole lot.
Your tone makes me unsure whether I should try to argue but, since when
does "safety" in programming languages have anything to do with static
as opposed to dynamic type-checking?
The notion of safety I know prescribes well-defined behavior in error
situations, and disallowing behavior that doesn't make sense from an
abstract point of view, which is roughly anything that exposes details
of the underlying machinery during computation, like the raw
byte-sequences denoting the abstract entities worked with. These are
also, from my knowledge, the main target of security exploits,
specifically memory unsafety.
If we treat safety/unsafety as a boolean, then the dynamically typed
languages you mentioned are safe, whereas C is not; both in terms of
types and memory, and memory safety is the security-relevant notion of
safety I know.
If we were to treat it as a continuum, I would rather call a type-safe,
memory-safe, dynamically typed language slightly less safe than a
type-safe, memory-safe, statically typed language, and I'm unsure how
much this notion of safety is relevant to security exploits.
The mention of speed, by the way, seems very off-the-mark.
I know nothing about any previous arguments you were in, but from these
three e-mails alone I'll sadly have to agree that you appear to have a
bias against so-called "dynamic" languages. :-)
Taylan
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-08 16:37 ` Taylan Ulrich Bayırlı/Kammer
@ 2014-03-08 16:47 ` Stefan Israelsson Tampe
2014-03-08 20:56 ` Mateusz Kowalczyk
2014-03-08 20:47 ` Mateusz Kowalczyk
1 sibling, 1 reply; 11+ messages in thread
From: Stefan Israelsson Tampe @ 2014-03-08 16:47 UTC (permalink / raw)
To: Taylan Ulrich Bayırlı/Kammer; +Cc: guile-user@gnu.org
[-- Attachment #1: Type: text/plain, Size: 2661 bytes --]
The beauty of scheme is that it is quite possible to design statically
typed meta language. And if we let the guile hacker doggies chew on the
guile stake a little bit more, you would also see a speedup of the
generated code that will essentially mean that just a tiny bit of C-code
needs to be written. In all a perfect setup for fast maintainable and
secure code. But the bit's needs to be in place. Why don't we try to copy
typed racket over to guile?
/Stefan
On Sat, Mar 8, 2014 at 5:37 PM, Taylan Ulrich Bayırlı/Kammer <
taylanbayirli@gmail.com> wrote:
> Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
>
> > On 08/03/14 00:32, Mark H Weaver wrote:
> >> Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
> >>> I doubt that going from a single inherently unsafe but bloody fast
> >>> language to slightly less unsafe but much slower language is an
> >>> advantage here…
> >>
> >> "Slightly less unsafe"? Seriously?
> >
> > Sure. You get rid of pointer arithmetic which is the beg evil in C but
> > you lose any kind of static typing. It's about as safe as Python, Ruby
> > and whatever new and hip dynamic language is popular today: not a
> > whole lot.
>
> Your tone makes me unsure whether I should try to argue but, since when
> does "safety" in programming languages have anything to do with static
> as opposed to dynamic type-checking?
>
> The notion of safety I know prescribes well-defined behavior in error
> situations, and disallowing behavior that doesn't make sense from an
> abstract point of view, which is roughly anything that exposes details
> of the underlying machinery during computation, like the raw
> byte-sequences denoting the abstract entities worked with. These are
> also, from my knowledge, the main target of security exploits,
> specifically memory unsafety.
>
> If we treat safety/unsafety as a boolean, then the dynamically typed
> languages you mentioned are safe, whereas C is not; both in terms of
> types and memory, and memory safety is the security-relevant notion of
> safety I know.
>
> If we were to treat it as a continuum, I would rather call a type-safe,
> memory-safe, dynamically typed language slightly less safe than a
> type-safe, memory-safe, statically typed language, and I'm unsure how
> much this notion of safety is relevant to security exploits.
>
> The mention of speed, by the way, seems very off-the-mark.
>
> I know nothing about any previous arguments you were in, but from these
> three e-mails alone I'll sadly have to agree that you appear to have a
> bias against so-called "dynamic" languages. :-)
>
> Taylan
>
>
[-- Attachment #2: Type: text/html, Size: 3349 bytes --]
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-08 16:37 ` Taylan Ulrich Bayırlı/Kammer
2014-03-08 16:47 ` Stefan Israelsson Tampe
@ 2014-03-08 20:47 ` Mateusz Kowalczyk
1 sibling, 0 replies; 11+ messages in thread
From: Mateusz Kowalczyk @ 2014-03-08 20:47 UTC (permalink / raw)
Cc: guile-user
On 08/03/14 16:37, Taylan Ulrich Bayırlı/Kammer wrote:
> Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
>
>> On 08/03/14 00:32, Mark H Weaver wrote:
>>> Mateusz Kowalczyk <fuuzetsu@fuuzetsu.co.uk> writes:
>>>> I doubt that going from a single inherently unsafe but bloody fast
>>>> language to slightly less unsafe but much slower language is an
>>>> advantage here…
>>>
>>> "Slightly less unsafe"? Seriously?
>>
>> Sure. You get rid of pointer arithmetic which is the beg evil in C but
>> you lose any kind of static typing. It's about as safe as Python, Ruby
>> and whatever new and hip dynamic language is popular today: not a
>> whole lot.
>
> Your tone makes me unsure whether I should try to argue but, since when
> does "safety" in programming languages have anything to do with static
> as opposed to dynamic type-checking?
There is of course more to safety than that but statically assured
safety is certainly a big deal. I think we could spend a whole lot of
time arguing here about what exactly makes for a safe language but the
thread isn't really about it.
My question is: how will the new libs written in Guile be assured to be
free of security bugs? I only pointed out that Guile itself does not
provide any automatic, static assurances that one could use. It is not
the case against Guile or Scheme or whatever, merely an observation.
> The notion of safety I know prescribes well-defined behavior in error
> situations, and disallowing behavior that doesn't make sense from an
> abstract point of view, which is roughly anything that exposes details
> of the underlying machinery during computation, like the raw
> byte-sequences denoting the abstract entities worked with. These are
> also, from my knowledge, the main target of security exploits,
> specifically memory unsafety.
This is why I mentioned that there also needs to be assurance that the
generated C parts are immune to such attacks.
> If we treat safety/unsafety as a boolean, then the dynamically typed
> languages you mentioned are safe, whereas C is not; both in terms of
> types and memory, and memory safety is the security-relevant notion of
> safety I know.
>
> If we were to treat it as a continuum, I would rather call a type-safe,
> memory-safe, dynamically typed language slightly less safe than a
> type-safe, memory-safe, statically typed language, and I'm unsure how
> much this notion of safety is relevant to security exploits.
I find type-safe and dynamically-typed to be a rather weird combination:
dynamic languages tend to pretty much have only a single type, with
many, many instances. Basically all functions take arguments of that
type and if the values don't match up, we get a run-time
error/exception/whatever it is. Comparing ‘types’ in such languages is
no different than comparing two integers. In any case, if you want to
discuss this further I suggest a separate thread or coming on IRC or
whatever. It is not a crucial point of this discussion.
> The mention of speed, by the way, seems very off-the-mark.
It was simply to point out an advantage of using C over using Guile.
Another would be the many eyeballs that looked at the existing library.
> I know nothing about any previous arguments you were in, but from these
> three e-mails alone I'll sadly have to agree that you appear to have a
> bias against so-called "dynamic" languages. :-)
I did not have any previous arguments of such nature on this mailing
list or the #guile IRC channel. I think Mark simply is a bit sour about
some totally unrelated arguments and feels the need to take it out on me.
> Taylan
>
Again, I'm not saying anything of the sort that Guile is unsuitable to
write a security-critical library in. I'm saying that it is not enough
to simply rewrite library in Guile: extra assurances are needed and I do
not see anywhere in the OP how those will be given. This is not a ‘Guile
vs C/Haskell/Python/anything’ thread, this is not a ‘Guile is unsafe’
thread, this is a ‘where are the assurances of the security of the new
libraries’ thread.
--
Mateusz K.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-08 16:47 ` Stefan Israelsson Tampe
@ 2014-03-08 20:56 ` Mateusz Kowalczyk
2014-03-09 0:40 ` Mike Gran
0 siblings, 1 reply; 11+ messages in thread
From: Mateusz Kowalczyk @ 2014-03-08 20:56 UTC (permalink / raw)
Cc: guile-user@gnu.org
On 08/03/14 16:47, Stefan Israelsson Tampe wrote:
> The beauty of scheme is that it is quite possible to design statically
> typed meta language.
Please spare me this approach. It certainly is possible but is a lot of
effort and you get a gimped version of existing languages but without
any real features. If you're going to design such a thing, why not
simply use a different language and expose bindings? I am unsure if
you're only mentioning that it is possible as thought or are actually
suggesting such approach.
> And if we let the guile hacker doggies chew on the
> guile stake a little bit more, you would also see a speedup of the
> generated code that will essentially mean that just a tiny bit of C-code
> needs to be written. In all a perfect setup for fast maintainable and
> secure code.
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.
> 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.
> /Stefan
--
Mateusz K.
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-08 20:56 ` Mateusz Kowalczyk
@ 2014-03-09 0:40 ` Mike Gran
2014-03-09 7:47 ` Mateusz Kowalczyk
0 siblings, 1 reply; 11+ messages in thread
From: Mike Gran @ 2014-03-09 0:40 UTC (permalink / raw)
To: Mateusz Kowalczyk; +Cc: guile-user@gnu.org
On Saturday, March 8, 2014 12:57 PM, Mateusz Kowalczyk <fuuzetsu@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.
This is could be said of any program written in purely functional style,
I suppose. So that's an advantage with respect to security.
>> 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?
But if software safety is your goal, I'd go with ADA.
Un-seriously yours,
Mike Gran
^ permalink raw reply [flat|nested] 11+ messages in thread
* Re: Writing libraries for C programs using Guile Scheme
2014-03-09 0:40 ` Mike Gran
@ 2014-03-09 7:47 ` Mateusz Kowalczyk
0 siblings, 0 replies; 11+ messages in thread
From: Mateusz Kowalczyk @ 2014-03-09 7:47 UTC (permalink / raw)
Cc: guile-user@gnu.org
On 09/03/14 00:40, Mike Gran wrote:
> On Saturday, March 8, 2014 12:57 PM, Mateusz Kowalczyk <fuuzetsu@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.
^ permalink raw reply [flat|nested] 11+ messages in thread
end of thread, other threads:[~2014-03-09 7:47 UTC | newest]
Thread overview: 11+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2014-03-07 8:22 Writing libraries for C programs using Guile Scheme Peter TB Brett
2014-03-07 16:30 ` Mateusz Kowalczyk
2014-03-07 16:36 ` Mateusz Kowalczyk
2014-03-08 0:32 ` Mark H Weaver
2014-03-08 3:50 ` Mateusz Kowalczyk
2014-03-08 16:37 ` Taylan Ulrich Bayırlı/Kammer
2014-03-08 16:47 ` Stefan Israelsson Tampe
2014-03-08 20:56 ` Mateusz Kowalczyk
2014-03-09 0:40 ` Mike Gran
2014-03-09 7:47 ` Mateusz Kowalczyk
2014-03-08 20:47 ` Mateusz Kowalczyk
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).