back to article Researchers forge secure kernel from maths proofs

Aussie boffins have developed an operating system micro-kernel mathematically established as free of many types of errors. The development points the road toward "safety-critical software of unprecedented levels of reliability" for applications such as aircraft and cars. The software - called the secure embedded L4 (seL4) …

COMMENTS

This topic is closed for new posts.
  1. Don Mitchell

    Theorem Proving

    There is quite a bit of that technology used in industry. Extensive theorem-proving scaffolding and refactoring to manage security relationships has been applied to the Windows kernel in the last few years.

  2. Suburban Inmate
    Terminator

    One step closer....

    ...to computers coding and debugging by themselves. We already have self modifying code, of sorts. A few more years and we'll only have to ask the computer what sort of program we want, or behaviour desired.

    "Today the Government announced that it had successfully completed the migration of all civil and military operations to the latest generation of server operating environment, programmed with the input of just 3 simple rules...."

  3. Anonymous Coward
    Anonymous Coward

    Interrupting

    My immediate thought was how are they modelling interrupts in their proofs? Those have caused mighty headaches to mathematically proved processors in the past - I can only imagine the same issues will arise with kernels.

  4. The Other Steve
    Boffin

    Hmm, puts me in mind of a Don Knuth quote

    "Beware of bugs in the above code; I have only proved it correct, not tried it"

  5. Anonymous Coward
    FAIL

    Mathematically verified, like RSRE Viper processor?

    And what happened to the RSRE Viper processor when the proof was proved to be not a proof ?

  6. Brian Miller

    How to get your grant money and spend it too

    Let me get this straight: they developed a mathematically correct kernel by analyzing C code, and then wrote the final kernel in C.

    I trust I'm not the only one who sees a flaw with this....?

    Will their product be part of the Obfuscated C contest? Under the "mathematically correct" category?

  7. Apocalypse Later

    Math mirth

    One of my math teachers once proved to a class that 1=2 using algebraic formula. None of us could spot the flaw (a concealed divide by zero). I hope these guys ran a subroutine to check all the divisors.

  8. vincent himpe

    'c' code ?

    are the bonking mad ? That language is flawed by design ... There is a reason it is called 'c' : that was the final grade it got when they handed it in ...

    have they tried analysing the bartender problem with that tool of theirs ?

    for people that don't know the bartender problem : 3 men walk in to a bar. and order a beverage,

    Beverage costs 10 pence. the bartender receives 30 pence. The innkeeper says : these are good customers give them a pence discount on their tab.

    the bartender can't split the 5 pence. so he gives each customer 1 penny back and keeps 2 for himself.

    from the customers perspective : they only paid 9 pence each.. 3x9 = 27 , add the two pence the bartender kept. total : 29 pence... where o where did the thirtied one go ...

  9. sT0rNG b4R3 duRiD
    Paris Hilton

    What about...

    1. The compiler compiling this code?

    2. The CPU it will be executing on?

  10. Brian Scott

    Title

    Unfortunately a mathematical proof of correctness may prove that some set of known types of bugs don't exist and it may prove that the program actually matches the specification. What it doesn't prove is that the program is what the customer wanted (i.e. the specification is never complete and will change over time so insisting on it being complete and static is a very good way to get a disappointed customer).

    Does proof of correctness result in code that is optimally able to be maintained (oops, sorry - if it starts out life correct then it never needs maintenance does it?).

    More importantly, our happy user needs to use this kernel to do some real work so they install a web server on it, along with php, then hire a cheap programmer that has read a book on PHP to write applications for it.

    The eventual end user knows nothing about any of this and compromises the integrity of the system by writing down passwords on sticky pieces of paper or surfing pr0n sites that use have bonus cross site request forgeries embedded in them....

    It may be nice to have a more robust Kernel but I think the money would be better spent on researching how to fix the real problems that plague computer systems.

  11. Anonymous Coward
    Welcome

    HAL far from foolproof!

    As I remember it, all you had to do was give him two contradictory orders at once at the same level of priority and he'd undergo a massive psychotic breakdown.... Using the Cretan paradox in one form or another to make a computer overload and blow up is the oldest trick in the sci-fi book.

    Similarly, in the context of this story, the fact that they've mathematically proved it to be formally correct really just means that now they're half-way to proving the overall formal system's Gödel statement, and thereby demonstrating that it is either incomplete or inconsistent. Well done them! I look forward to the inevitable future moment when this proven-mathematically-correct system goes completely haywire and starts spewing out random garbage!

  12. Denarius
    Paris Hilton

    Next !

    So, a team of clever people, over years, has recreated a light version of secure BSD *nix.

    But, mathematically proven, like the heavier than air machine cant fly, radio coils must be over a specific (big) size...

    Now we start checking the hardware BIOS, silicon logic in the CPU and eventually the firmware in the attached devices.

    Paris, because even she knows when enough is enough, sort of.

  13. Big-nosed Pengie
    FAIL

    @Don Mitchell

    "Extensive theorem-proving scaffolding and refactoring to manage security relationships has been applied to the Windows kernel in the last few years."

    Oh shit. It clearly doesn't work then.

  14. CArguin
    Linux

    But it's not Linux

    The current by-line on the front page is "Computer scientists claim to have built a Linux kernel for embedded...", but nothing here says anything about it being Linux related; indeed, it's a microkernel. It could possible run linux inside the proven correct microkernel, but let's not confuse the issue.

  15. Rodyland
    Thumb Down

    Proves nothing

    Maybe it's just me, because I'm not usually the first to think of these sorts of things, but...

    Isn't the idea of a formally proven kernel written in C nothing more than an academic exercise without a formally proven C compiler?

    Not to mention the CPU and chipset as well, while we're at it.

  16. Anonymous Coward
    Boffin

    @ Math mirth

    Oh you crazy Math people!

    Your life must be so full.

    The olde: concealed divide by zero trick eh?

    An oldie but a goodie!

  17. Michael H.F. Wilkinson Silver badge
    Boffin

    @The Other Steve; @Brian Miller

    @The Other Steve: Nice one, Dijkstra on the other hand got angry when you suggested testing something he had proved.

    @Brian Miller: Not a flaw at all. It is possible to write secure C, just as it is possible to write secure assembly (after all, any secure code must be secure machine code at the final crunch). So long as you have a secure C compiler (mathematically correct) you are OK. Exactly because C is so small, as a language, it is less hard to prove correct.

  18. sT0rNG b4R3 duRiD
    Thumb Up

    Ah.. now I get it...

    Researchers "forge" secure kernel from maths proofs

    Good one...

  19. John Smith 19 Gold badge
    Thumb Up

    AC@23:38

    IIRC VIPER hit trouble due to the team assuming the implementation tools (turning the absctract register based machine desing into actual gates on chip) had no errors in them. This was incorrect. When the design had demonstrated bugs the project hit the skids.

    Lesson. You need to verify the *whole* toolchain. Just because *most* users of the (commercial) design tools have no problems does not make them problem free.

    Going from memory (V. old Byte article early 80s) The architecture was basically a 16 bit 6502. The 1st implementation was a gate array using a series of finite state machines using a 26Mhz clock to get 1MIPS. I seem to recall some fairly simple changes upped the speed quite a lot but made the verification harder (verification being the actual project focus)

    I think RSRE had a buy British policy so when to their chums at GEC for that stuff. Who knows what would have happened if they had used VLIS logic instead (company that fabbed the ARM series).?

  20. TeeCee Gold badge
    FAIL

    Oh really?

    '......a HAL-like system that's "foolproof and incapable of error".'

    Yeah, 'cos an AI that cannot resolve conflicting orders is definately foolproof and that it then goes on to attempt to exterminate its meatsack colleagues is merely proof of its incapability of error.

  21. Charles Manning

    Wht the Tux

    As far as I can make out this isn't a Linux kernel.

  22. Anonymous Coward
    Paris Hilton

    It depends on the model

    I suppose the proof starts of a bit like this:

    Suppose there is ...

    and then goes on to use base assumptions to mirror physical events controlled by the kernel.

    Which is ok, fine and dandy - it really is a brilliant start but kernels tend to operate with voltage changes effected at very high frequencies yes?

    So there will always be a physical element that the proof cannot completely cater for?

    So, good model = good proof.

  23. Bilgepipe
    Gates Horns

    Ahh, Maffs

    First flaw identified in 3.....2.....1.....

  24. Ken Hagan Gold badge

    Proven, for some value of "proof".

    The article mentions C, but that is known to have several internal contradictions and *that* would make a mathematical proof impossible. However, one could (with some effort) go through all those inconsistencies and resolve them one way or the other and end up with a C-like language that was well-defined, and then use *that* to produce a kernel that was proven. That would be a useful exercise if it yielded new techniques. (I don't want to mock, too much.)

    For example, you might write a compiler for the new language. Of course, then you'd need to prove the compiler. And you'd only be able to run the compiler on a proven operating system, which you don't have yet. And you'd only be able to run either on proven hardware, which I suspect also that you don't have yet. (OK, just a little.)

    But all that is for a *mathematical* interpretation of "proven correct", which is a boolean attribute, whereas engineers recognise a continuum of...

    Proven wrong

    Smells bad

    Compiles, but I haven't tried it out yet.

    I'm quite proud of this and willing to publish it.

    I'm quite proud of the test suite, and willing to publish that too.

    I'm quite proud of the original requirements spec, and willing to publish even that.

    I have professional indemnity insurance that covers this.

    (That's not mockery by the way. Outside of the maths department, no-one ever *proves* anything, but people sometimes put their money where their mouth is and you can tell a lot by just how much money they, or more accurately their insurance companies, put up.)

  25. Mage Silver badge
    Flame

    What no Razor

    Using C?

    mad. A write only portable Assembler. Hardly a decent High Level Language.

    Occam, Modula-2, Oberon, maybe C# or C++, not C

  26. Rob Beard
    WTF?

    Linux

    Are you sure it's a Linux kernel?

    Linux is a monolithic kernel not a micro kernel. GNU Herd is a micro kernel.

    Also following the links, the only reference to Linux is that it will run on top of this kernel, not that this kernel is derived from Linux.

    Rob

  27. amanfromMars 1 Silver badge

    I wish them luck but .....

    "All this heavy mathematical lifting means that the kernel ought to be immune to common types of attack, such as buffer overflows."

    And the first half hearted assault which results in a buffer overflow will render their testing model fundamentally flawed and their promises just so much hot air/commercial posturing/spin?

  28. It wasnt me

    @Apocalypse Later

    Go get-em !

    Im sure they didnt think of that.

    Give this man some grant money.

    Or maybe they did look for the completely fu&*ing obvious stuff before they went on to the more tricky stuff.

  29. Anonymous Coward
    Anonymous Coward

    Acronyms..

    Australia's Information and Communications Technology Centre of Excellence (Nicta).

    AICTCE

    NICTA

    Yep exactly!

  30. Tom 7

    @Apocalypse Later

    He might have fooled you into thinking 1=2 but he didn't prove it mathematically - its the same technique used by city types to prove they're useful. Works on politicians but not reality.

    @Don Mitchell - you need to apply it to the whole 'kernel' to be of any use, and then be prepared to fix the system when you find problems - but as that would stop a lot of it functioning usefully....

  31. Graham Marsden
    Boffin

    "foolproof and incapable of error"

    But, as the old quote has it: "It is impossible to make anything foolproof because fools are so ingenious."

  32. Matt Bryant Silver badge
    Stop

    Erm...... remember that whole bumblebee thing?

    Whilst I'd love to stand up and wave the flag for Linux, I get a bit worried whenever a boffin stands up and says something is "mathematically proven". Maths is just modelling tools that allow us to describe real world events in a manner some can understand, and often include plenty of assumptions. Of course, if your mathematical model is flawed or just wrong, then you get some fun scientific gaffes such as the so-called proof that bumblebees can't fly. Actually, if you use the standard aerodynamic models the maths says they can't, but if you use the special models for helicopter flight then it all looks much better for our fuzzy friends. It's probably a good thing bumblebees put a lot more faith in empirical testing rather than mathematical theorems, and so do I - until it is thoroughly tested in a real environment, nothing is proven.

  33. Anonymous Coward
    Go

    Less cynicism?

    @Suburban Inmate

    The proof are being done with Isabelle, which is an "interactive theorem prover". Essentially this means that the computer is doing the number crunching and humans are directing the proofs and doing the clever stuff.

    @Anonymous Coward

    The main problem there was folks making overly bold claims. The proofs themselves were valid, just not as far reaching as some thought. Things have progressed since then but there are still boundaries with every formal verification.

    @Brian Miller

    Your comment makes no sense. They used a theorem prover, called Isabelle, which is written in Standard ML. This supports doing proofs in higher-order logic (a formal mathematical logic). They used this logic to model the semantics of C code. This semantics is then used to verify correctness properties for the source code of the Kernel.

    @Apocalypse Later

    This is the entire point of using an interactive theorem prover. It should guarantee that there are no holes in your proofs. The main problem is making sure you've proved exactly the right thing i.e. that your models are right and that they are detailed enough.

  34. Steen Hive
    WTF?

    L4?

    "Computer scientists claim to have built a Linux kernel for embedded mission-critical systems that maths proves is free of many types of errors"

    Eh, L4 isn't Linux, it's Mach.

  35. James 47

    pffffffffffft

    how do you model faulty hardware or suffering a power cut?

  36. This post has been deleted by its author

  37. AndrueC Silver badge
    Stop

    Yeah..right.

    To err is human. To screw up completely requires a computer.

  38. Joe M
    Happy

    Yeah, yeah!

    Remember this old logos: In theory, theory and practice are the same, but in practice they are not.

    If you work in this game long enough you realise that a real-world OS running on real-world hardware is not deterministic. The theory says that it is and if everything runs well, it is; but nothing runs well all the time and, alas inevitably, red faces all round when lots of great mathematics go up in a puff of "alpha particle induced memory error" smoke (or something similar).

    Cast back to LTCM Ltd. and the summer of 1998. Hubris before the fall!

    (Of course there is nothing wrong, and everything right, with a whole bunch of real smart guys carefully poring over kernel code, automated or not, and shaking out as many bugs as possible. Should happen more often.)

  39. Nigel 11

    Missiles?

    Although reliability of missile guidance systems is important, I'd have thought that the military would happily trade a 1% chance of post-launch system failure for things like a bigger payload or a better ability to deal with enemy countermeasures. (And 1% is orders of magnitude worse than today's commercial operating systems would give them).

    If this kernel really is a major step in upwards reliabiliy, I would have thought the most likely applications would be civilian. Things like self-driving cars, or civil aviation autopilots and fly-by-wire systems, or automated railway or air-traffic control.

  40. TimC
    WTF?

    Linux?

    Headline - "Computer scientists claim to have built a Linux kernel for embedded mission-critical systems that maths proves is free of many types of errors"

    Um, L4 is _not_ Linux guys .. although OKL version of L4 can run virtualised linux in a process...

  41. Annihilator

    @Matt Bryant

    "It's probably a good thing bumblebees put a lot more faith in empirical testing rather than mathematical theorems, and so do I - until it is thoroughly tested in a real environment, nothing is proven."

    Nothing is ever proven. Because A has happened n times, you can never be 100% sure that A will happen on the n+1st occurence. You just gain more confidence. Not that I think bumblebees are too worried about their tried and tested technique failing them tomorrow.

    Daaaaaiiiiiissssyyyyy daaaaaiiiiisssyyyy, ggiiiiiiveeee meeeee youuurrrrr annsssswwweerrrrr trruuuuuueeeeee. From what I can tell, HAL was never built on the 3 laws of robotics. RoboCop's Prime Directives, maybe. Dick? You're fired!

  42. The Commenter formally known as Matt
    Boffin

    @vincent himpe

    I dont get it, admittedly I've never heard of the bartender problem, but essentially you are saying

    30 - 3 + 2 = 29 but you think it should equal 30?

    Confused...

  43. Nick Ryan Silver badge

    Scared...

    Why am I always scared when mathematicians play at programming computers?

  44. MnM
    Paris Hilton

    @vincent himpe

    That tool of theirs would laugh in the face of your puny bar-man problem with its misdirection subroutine. You don't impress me (but fwiw it's a point well made).

    For me, it's only secure if Paris says so.

  45. regularfry
    Stop

    Ok, time to stop laughing.

    Ok, stop. There's a truism that applies in situations like this. If I, as a lay-person, can spot a problem with some expert's (or group of expert's) work within 30 seconds of hearing about it, it's fairly likely that they will have thought of it too. This makes nay-saying on that basis pretty pointless. Apart from anything else, it's boring and makes you look like an idiot.

    Everyone should really read http://ertos.nicta.com.au/research/l4.verified/proof.pml to see what the researchers are actually claiming, and see if you still think that a kernel which is, for instance, *completely immune* from buffer overflows, pointer errors and memory leaks (given the assumption constraints) is a waste of time.

    For my money, *anything* that raises the security bar is a good thing.

  46. John H Woods Silver badge
    FAIL

    @bartender problem / vincent himpe

    You are confused.

  47. chr0m4t1c
    Stop

    @vincent himpe

    You're making the mistake of putting numbers on the wrong side of the equation.

    Here:

    One beer is 10p (I wish!)

    Bulk discount, three beers for 25p.

    Three men each put in 9p, thus giving the bartender 27p for three beers - so they get 2p change.

    Bartender gets to keep the 2p change (as a tip, presumably). Nothing has gone anywhere.

  48. Anonymous Coward
    Anonymous Coward

    @ The Commenter formally known as Matt

    Don't be confused, vincent is just an idiot that seems to think that a mathematical problem used to trick high school kids is somehow relevant to formal mathematical proofs.

    He even suggests C is fundamentally flawed, which is interesting seeing as like 99% of computing systems around today run on it.

    C isn't fundamentally flawed, there are just bad programs who can use it incorrectly allowing issues to arise because they simply didn't understand how to program properly.

  49. Hugh_Pym

    @Annihilator

    Can you provide a reference for the aeronautical engineer that proved mathematically that bumble bees cannot fly? No you can't it's an urban myth.

    I think the problem is really that mathematical proof is indeed proof ... within certain limits. The proof it the easy bit it's the limits that are the bastard.

  50. Anonymous Coward
    Anonymous Coward

    Not a Linux kernel

    The summary on the front page says that this is a Linux kernel; it isn't (there's a clue in it being a microkernel). It can run a para-virtualised version of Linux and - in principle - other operating systems in this way. However, only the functionality provided by this secure kernel is "proven".

  51. Karim Bourouba
    Pint

    @ Steve Hive

    L4 isnt Mach as much as it isnt Linux.

    I think we can consider L4 to be the cousin of Mach?

  52. P. Lee
    Boffin

    Einstein addressed this

    "As far as the laws of mathematics refer to reality, they are not certain, as far as they are certain, they do not refer to reality."

  53. AlistairJ

    Huh you lot

    We in the chip industry use formal proofs on real projects.

    These days we commonly use formal proofs to compare gate level implementations of designs (from automated design tools) with the original design in a high-level language. It offers a much more complete verification than mere simulations. Sounds like this could have been useful on that crappy Viper project (RSRE = loud harmonica).

    We also use formal proofs on high-level designs, although these methods have their drawbacks and limitations it has to be said.

    Mind you, I would take anything coming from a bunch of Aussie academics with a large pinch of salt. Jeez they can't even spell their own initialisms.

  54. David S

    @Apocalypse Later

    Hey, I remember that proof! I was so impressed with it when I first saw it too...

    Happy days...

    Ring a bell? http://www.math.utoronto.ca/mathnet/falseProofs/first1eq2.html

  55. Anonymous Coward
    WTF?

    Bartender problem

    Sorry , perhaps I'm too dumb to be confused by this - but the men get 3 beers and the Bartender gets to keep 27p. So he lost 3p on the sale instead of 5p. Wheres the trick question?

  56. The Indomitable Gall

    Bartenders (re: 'c' code ?)

    @ vincent himpe

    What's your point? The bartender's problem is a matter of "blinding with science". It's works by assuming false premises, and expressing them in such a matter-of-fact way that the listener takes them as given.

    In fact, I've been asked variations on the bartender's problem without actually knowing the answer themselves. When I explain how it works, I sometimes find they're so trapped in the illusion that they refuse to accept the answer. (Are you one of these...?)

    The thing with computers is that yes, they are reliant on valid input, and false premises programmed in can be a stopping point, but if they have all the appropriate information, their lack of a brain means there's no psychological tricks you can employ to convince them not to explore the full search space.

  57. Steen Hive
    FAIL

    @ Karim Bourouba

    Fail & Me. Yeah of course when correcting an obvious error, I would be guaranteed to make one myself and mistakenly not type "L4 isn't Linux, it's more like Mach". :-)

    L3 & L4 were ostensibly designed to overcome some of the performance limitations of Mach.

  58. Alan Douglas

    AManFromMars?

    I understood AManFromMars comment, in fact it's what I wanted to say. Should I be worried?

  59. MnM

    @The Indomitable Gall

    'When I explain how it works, I sometimes find they're so trapped in the illusion that they refuse to accept the answer.'

    I've had the exact same odd experience. Otherwise genuinely intelligent people will say

    things like 'this shows that maths is flawed'. I'm sure they're secret celestine prophecy readers, and they are everywhere.

  60. blackworx
    Paris Hilton

    Whoosh

    This kind of stuff

    .

    .

    .

    .

    .

    .

    .

    .

    .

    My head

  61. Graham Bartlett
    Flame

    All these folk checking the gift horse's teeth

    I don't get it. I really don't. A group of people have gone to the trouble of putting together a microkernel that's provably without bugs in the C code, and they're getting slated for it? It's like SpaceX or someone saying "we've invented a rocket that'll get us to Pluto and back in 10 minutes, but we need to fire it up outside the atmosphere", and then everyone taking the piss instead of saying "cool, let's figure out how to get it in the Space Shuttle".

    Sure, it requires a known-good C compiler. If you need this for your business, you can work on it. And if you want to move to a new platform, you don't need to develop a whole new microkernel, just a new C compiler. Certainly there are ambiguities in the C language, but they're known and well-documented, which is why coding standards such as MISRA-C exist to guide coders around those ambiguities. (Not heard of MISRA? Then you don't know enough to have an opinion on the subject of safety-critical software.) Actually, optimisation is usually the problem with compilers - provably-correct compilation from a line of C to lines of assembler is fairly straightforward (at least without interrupts getting in the way), but it's slower and less efficient.

    @Annihilator: "Nothing is ever proven"? Sorry, but 2+2 still equals 4 and parallel lines don't meet in finite space, regardless of day of the week, phase of the moon, or 50 trillion years in the future. Get a grip.

  62. Annihilator

    @Hugh_Pym

    Hi Hugh - I didn't claim that bumblebees can't fly. I know that it's an urban myth - came from a drunk aeronautical engineer who worked out that a bumblebee can't fly like a conventional fixed wing aircraft. Problem is that they don't try to fly like that - if it stops flapping its wings, it'll fall out the sky - it won't glide.

    However, with reverse-pitch semirotar blades they fly just fine.

    @Graham Bartlett - 2+2 equals 4 is an extension of the definition/assumption/rule that 1=1 and permutational mathematics. 2+2=4 doesn't "prove" anything. Parallel lines never meeting are again a definition of finite space, and not there to prove anything. Do a maths degree.

  63. Phil Rigby
    Grenade

    Why only war?

    Assuming that we can get a fool-proof system, why is the first practical use have to be for a war/military solution?

    "The technology is designed for complex embedded systems where reliability is of critical importance, so applications in missiles and other defence-related systems are an obvious application of the software."

    How about a system to cure HIV or cancer? How about a way to mass-produce food for drought-ridden countries? Does it have to be for blowing people up?

    Grenade icon for the irony.

  64. Rob Dobs
    Stop

    @ vincent himpe

    uhmm.... customers paid 27p, bartender stole 2p - the "oher pence is one of the other 25 the bar is keeping in the til to pay for the drinks.

    The incorrect assertion is in the statement where you are taking the total of what the people paid, and adding what the bartender stole - and expecting this for some reason to equal 30.

    You also say "they customers paid 27, the bar owner was paid 25 and the bartender stole 2p - that totals up to 54p - where did the extra 24p come from??" If you mis-state the facts and add negatives to positives you can come up with all kinds of numbers.

    30p goes in til

    5 p comes out

    1p goes to each customer (3p)

    2p goes in sneaky pete the bartenders pocket

    25p left in til,

    customers paid 27p

    bartender stole 2p

    bar get 25 (2 short of what owner wanted)

    All this adds up just fine.

    Thanks for posting though, I did have to look for a second to find the false statement..... a good mind exercise in being careful what crap you listen too - just look at the US healthscare debate.

  65. Sureo
    Happy

    On a lighter note....

    Canada's former prime minister Jean Chretien once said,

    "No, a proof is a proof. What kind of a proof? It's a proof. A proof is a proof, and when you have a good proof, it's because it's proven."

    This has given Canadians much needed hilarity, something sorely missing in our politics and culture.

    http://www.canadaka.net/video/293-jean-chretien-a-proof-is-a-proof.html

  66. adrian sietsma
    Black Helicopters

    @vincent himpe : re c

    c is _just_ a language. It allows one to code instructions for a cpu. Get it wrong and it'll hurt you; so will running with scissors. You want I should write a microkernel in vb.NET because it's "manged" and "foolproof" and hides all those scary memory allocations from you ?

    meh

    (that's not a helicopter, it's a squashed bug)

  67. Anonymous Coward
    Anonymous Coward

    @Graham Bartlett

    "A group of people have gone to the trouble of putting together a microkernel that's provably without bugs in the C code, and they're getting slated for it?"

    From the Great Book of Lies:

    "In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. Functional correctness refers to the input-output behaviour of the algorithm (i.e., for each input it produces the correct output)."

    (http://en.wikipedia.org/wiki/Program_specification)

    No mention was made in the article that the specification that the code was checked against was similarly proved to be mathematically correct, so really what we've got is a microkernel that's free from coding bugs but not necessarily free from logic-related bugs. Which means you could have a rocket that will always, always, always crash 20m from the launch site even though the customer wanted a long-range ballistic missile.

    When the mathematicians can prove the specification is free from fuckwittery and the program is functionally correct that will be a good day. This announcement is merely a guarantee that the build quality is up to the management team's brainstorming sessions.

  68. This post has been deleted by its author

  69. Anonymous Coward
    Boffin

    not too many software engineers

    hereabouts, it seems.

  70. Vanir
    Coat

    C Specs

    Does the C language have a formally defined specification using mathematical notation?

    C has a syntax dependent on context.

    Perhaps we should look at our code as a conjecture that requires other people, erm customers, to prove correct or not. But, if there is no spec then the code is not a conjecture but just a programmer's doodling.

    Now let's shoot the colonel with void pointers and see what type of wounds we inflict.

  71. Charles Manning

    re: Why C?

    C is probably an OK choice. It is a very simple, and therefore verifiable, language.

    C++ is way, way, more complex than C. Complexity means failures.

    Modula2, erlang and other languages that help detect runtime errors, but that's not really a help: the system still fails. At least when your brakes fail you can die with the knowledge that it was an array bounds exception that killed you.

  72. Michael H.F. Wilkinson Silver badge
    Black Helicopters

    @Phil Rigby: Why only war?

    - Assuming that we can get a fool-proof system, why is the first practical use have to be for a war/military solution?

    Answer: only fools make war

  73. A J Stiles

    @ vincent himpe

    Others have already corrected you on the bartender problem, so I'll refrain from pointing out that there's no reason why the amount originally paid by the customers minus the change returned to the customers (= price charged for goods plus amount retained by bartender) plus the amount stolen by the bartender (already accounted for) should add up to the amount originally paid by the customers. I should know, I've got an engineering degree (from the days when that entailed more maths than a maths degree) and I've worked in a bar. It's a bit like Abbot and Costello's proof that 13 * 7 = 28.

    Your comments on languages also miss the point. How do you know that the compiler for your latest fancy-arsed language is mathematically correct? At least C instructions can be mapped to machine instructions; and the ARM architecture on which they intend to run it is famous for its hardwired instruction set (no microcode). Meaning that there's a mapping from C instructions to logic gates. That's about as verifiable as you can get!

  74. Lost in a maze of twisty messages, all alike.

    @vincent himpe

    you appear to have a sign error in your algorithm, maybe you should have verified it mathematically ...

This topic is closed for new posts.