Slashdot is powered by your submissions, so send in your scoop


Forgot your password?

Comment Re:Great work, but... (Score 1) 517

Haskell's garbage collection works (or should work) based on formal inference -- seeing as they translated the haskell to C manually, they would have proved the garbage collection as part of the deal. Also, haskell's prelude and basic libraries have already been formally proven.

Because of formal inference, a good Haskell compiler knows exactly when and what will be garbage collected at compile time - there is no mark-and-sweep approach like Java. It's no worse that manually freeing stuff in C, in fact it's substantially better.

Comment Re:The Amiga Hand? (Score 1) 517

Do you know what "formal" means? It's talking about "formal" as in programs as formal systems, a branch of logicianship that allows you to reason about computation. I would much rather use a completely untested, but entirely formally proven operating environment than a long-lived unproven one. We just haven't gotten to the point where we have proved enough software yet.

Comment Re:Thank goodness (Score 3, Insightful) 517

Dude, can C's types be reasoned by formal inference? No. Hence, C does not follow typed logical calculus.

C doesn't follow boolean logic either, actually, it just maps to assembly instructions. The best thing you could do to reason about C is to use Dijkstra's proof method which is impractical in a large scale and easy to screw up.

Comment Re:spec? (Score 3, Interesting) 517

1) L4 is a microkernel. You have no idea what you're talking about. If L4 works, then you could apply similar principles for all the other servers that run in kernel space.

2)This is the largest formal proof ever done in this sort of field. Seriously, the results are not immediately useful, but it's a good start.

Disclaimer: I have worked at NICTA in the past.

Slashdot Top Deals