Return Styles: Pseud0ch, Terminal, Valhalla, NES, Geocities, Blue Moon. Entire thread

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.
Newer Posts
Don't change these.
Name: Email:
Entire Thread Thread List
All trademarks and copyrights on this site are owned by their respective parties. All comments and posts are the responsibility of their own posters.
- Tinychan + 2ch Mode -