/prog/ - Can a program can do exactly some given task?

Name: Anonymous 2011-11-28 12:33

Is there any way to be sure that a given program will do exactly a specific task?
Let's say I want to make a round-robin scheduler. Is there some way that I can be sure that certain program I've written will do exactly that?

Name: Anonymous 2011-11-28 12:42

http://coq.inria.fr/

Name: Anonymous 2011-11-28 12:58

What you're talking about is Formal Verification:
http://en.wikipedia.org/wiki/Formal_verification

It's a royal pain in the ass to do, only worth doing when it's truly _critical_ something is correct (NASA for example)

Name: Anonymous 2011-11-28 12:59

>>3
It's only a pain because you use C++.

Name: Anonymous 2011-11-28 13:32

>>4
Using lithp you don't make formal verification easier,
you make programming harder.

Name: Anonymous 2011-11-28 14:50

>>5
sage

Name: Anonymous 2011-11-28 17:51

How much confidence do you want?

Do you need to prove it absolutely? 

| Yes. -> You'll need something like Coq.

| Not really. -> Use an ML.

BitC was going to include a prover, but they eventually decided that it all comes down to a matter of confidence and the prover didn't add enough, and nobody would use it. Personally I'd like to make selective use of a prover but doing a whole nontrivial program sounds insane to me.

Name: Anonymous 2011-11-28 18:28

There's no way to know for sure. No way. No way.

Everything is based on baseless logic. Even reality itself is based on baseless logic.

Name: Anonymous 2011-11-28 18:34

>>8
I think he means that it will do what you think it does on a Turing machine.

Name: Anonymous 2011-11-29 5:26

Even reality itself is based on baseless logic.
And yet we think, therefore we exist, which is enough for me.

Name: Anonymous 2011-11-29 8:16

<---check 'em dubz

Name: Anonymous 2011-11-29 10:40

It's pretty easy if you've read your SICP.

1) Figure out how you expect a round-robin to react

2) theorize an "effective" strategy for implementing that reaction

3) implement that reaction

There, you've created a round robin.

Name: Anonymous 2011-11-29 14:02

>>12
Lisp is shit.

Name: Anonymous 2011-11-29 18:31

>>8
Even reality itself is based on baseless logic.
Your statement is based on baseless logic.

Reality is not the product of rational thought, thank god.

Can a program can do exactly some given task?

1 Name: Anonymous 2011-11-28 12:33

2 Name: Anonymous 2011-11-28 12:42

3 Name: Anonymous 2011-11-28 12:58

4 Name: Anonymous 2011-11-28 12:59

5 Name: Anonymous 2011-11-28 13:32

6 Name: Anonymous 2011-11-28 14:50

7 Name: Anonymous 2011-11-28 17:51

8 Name: Anonymous 2011-11-28 18:28

9 Name: Anonymous 2011-11-28 18:34

10 Name: Anonymous 2011-11-29 5:26

11 Name: Anonymous 2011-11-29 8:16

12 Name: Anonymous 2011-11-29 10:40

13 Name: Anonymous 2011-11-29 14:02

14 Name: Anonymous 2011-11-29 18:31