Pavel,
This brings us to the area of realizability: proofs and types :-) In fact,
the interesting thing is that for constructive logics once we have
the proof we also have to program. Some people have been extending this
paradigm towards classical logic using control operators.
A bit tricky though.
This is all great stuff, but I haven't seen it used in real world
applications. This is a challenge!!!
Regards,
-- Dirk
"Pavel Kankovsky"
<peakat_private To: secprogat_private
ff.cuni.cz> cc:
Subject: RE:Writing Secure code[update]
03/01/2003 20:00
On Wed, 1 Jan 2003, charles lindsay wrote:
> Personally, I have very little faith in proof of correctness (a baase
> requirement for A1), as most proofs tended to be larger than the code
> they were trying to prove.
Verification of formal proofs is trivial and a trained monkey can do it
(assuming a sane logic system with a sane proof system is used).
--Pavel Kankovsky aka Peak [ Boycott Microsoft--http://www.vcnet.com/bms ]
"Resistance is futile. Open your source code and prepare for assimilation."
**********************************************************************
This email and any files transmitted with it are confidential and
intended solely for the use of the individual or entity to whom they
are addressed. If you have received this email in error please notify
the system manager.
**********************************************************************
This archive was generated by hypermail 2b30 : Tue Jan 07 2003 - 13:49:49 PST