[SystemSafety] proofs

[paul_e.bennett at topmail.co.uk]

On 23/11/2018 at 12:10 PM, "Peter Bernard Ladkin" <ladkin at causalis.com> wrote:
>
>Paul,
>
>how is what you envisage different from strong typing + pre-
>/postconditions?
>(The example you give fits that description.)

My preferred programming environment is generally untyped unless
the programmers themselves force that by their own extensions to the
basic language. There is, though, a very clear data passing mechanism
which is always used and the declarations will refer to the intended type
that the function will handle. Hence, stating what pre-call data is available
and what post-call data is produced in the documentation allows others
selecting the function see if it fits their needs.

The difference I see, is that the compilers (and it is possible in my systems
to have many of those, but they are all quite simple single focus) do not do
the automated checking that you might be implying by your own viewpoint.

Regards

Paul E. Bennett IEng MIET
Systems Engineer
Lunar Mission One Ambassador
-- 
********************************************************************
Paul E. Bennett IEng MIET.....
Forth based HIDECS Consultancy.............
Mob: +44 (0)7811-639972
Tel: Due to relocation - new number TBA. Please use Mobile.
Going Forth Safely ..... EBA. www.electric-boat-association.org.uk..
********************************************************************