4 ms·

I remember asking the question on a stack-overflow site in 2015. https://cs.stackexchange.com/questions/45348/why-does-this-sort-algorithm-work https://cs.stac

I remember asking the question on a stack-overflow site in 2015. https://cs.stackexchange.com/questions/45348/why-does-this-sort-algorithm-work https://cs.stackexchange.com/questions/45348/why-does-this-s... And it was answered successfully by pointing the same invariant they point in the paper. I remember finding this program through via automatic program search, so the algorithm and the question of why it works as probably been discovered many times. If only we had something that would allow to surface information from the vast amount of data available...

Cryptonic 5y ago
Maybe there gotta be a paper or it does not exist xD
jvanderbot 5y ago
Write it down or it didn't happen. More directly, write down the result separate from the method or it won't be discovered by the right audience.
somenewaccount1 5y ago
Yes, but you asked a computer science question with computer code instead of "pseudo code and arguments of correctness.", as Rafael kindly reminded you. :)
- civilized 5y ago
  That comment was a bit of an eye-roller. The post is perfectly clear as it stands.
  - liversage 5y ago
    The original question contained a sizeable chunk of what looks like C#. It was then edited and made much clearer perhaps in a response to the comment.
  - svat 5y ago
    See the edit: https://cs.stackexchange.com/review/suggested-edits/26152 https://cs.stackexchange.com/review/suggested-edits/26152
- aasasd 5y ago
  More like, GistNoesis used 0-based arrays and the paper uses 1-based arrays. “Arguments of correctness” sounds like Rafael basically told GistNoesis to answer themselves, which is of course a widely spread attitude on SE.
gnramires 5y ago
I think we should start recognizing more alternate information sources, such as blogs and stack exchange (i.e. attribute scientific credit and recognition to those posts). Of course traditional scientific publishing has its place (including the care for methodology and source citation)... but many people will search directly those websites instead, so clearly it's an important emerging source of information and discovery.
aasasd 5y ago
Wait a minute! What the hell is ‘automatic program search’? Is it like with Malbolge where the first working programs had to be written through brute-force search?
- GistNoesis 5y ago
  You define some test-unit cases, input-output pair. You define some elementary blocks like in scratch (Blockly). And you try to randomly assemble the blocks so that they respect the type constraints. And you score your program based on the number of test case it got right. For this simple problem, naive random search was all that was needed. (less than 100k programs evaluations) But for more advanced cases you could use something like Genetic Programming with Koza's Automatically Defined Functions where you build an intermediate library of useful blocks. Now one would use deep learning and produce source code directly with some tool like Copilot and run it until it passes all tests. Or if you want to get your hands dirty, you can re-implement the old school methods and use a neural network to make the pick decisions instead of a random pick. Once you have programs that pass all test cases, you can try to prove correctness (that's more something like HOL-Light would do) and whether or not they are equivalent (and equivalent to a formal specification) and optimize them further by transforming the program.
  - aasasd 5y ago
    Interesting, thanks!

Cryptonic 5y ago

Maybe there gotta be a paper or it does not exist xD

jvanderbot 5y ago

Write it down or it didn't happen. More directly, write down the result separate from the method or it won't be discovered by the right audience.

somenewaccount1 5y ago

Yes, but you asked a computer science question with computer code instead of "pseudo code and arguments of correctness.", as Rafael kindly reminded you. :)

civilized 5y ago
That comment was a bit of an eye-roller. The post is perfectly clear as it stands.
- liversage 5y ago
  The original question contained a sizeable chunk of what looks like C#. It was then edited and made much clearer perhaps in a response to the comment.
- svat 5y ago
  See the edit: https://cs.stackexchange.com/review/suggested-edits/26152 https://cs.stackexchange.com/review/suggested-edits/26152
aasasd 5y ago
More like, GistNoesis used 0-based arrays and the paper uses 1-based arrays. “Arguments of correctness” sounds like Rafael basically told GistNoesis to answer themselves, which is of course a widely spread attitude on SE.

gnramires 5y ago

I think we should start recognizing more alternate information sources, such as blogs and stack exchange (i.e. attribute scientific credit and recognition to those posts). Of course traditional scientific publishing has its place (including the care for methodology and source citation)... but many people will search directly those websites instead, so clearly it's an important emerging source of information and discovery.

aasasd 5y ago

Wait a minute! What the hell is ‘automatic program search’? Is it like with Malbolge where the first working programs had to be written through brute-force search?

GistNoesis 5y ago
You define some test-unit cases, input-output pair. You define some elementary blocks like in scratch (Blockly). And you try to randomly assemble the blocks so that they respect the type constraints. And you score your program based on the number of test case it got right. For this simple problem, naive random search was all that was needed. (less than 100k programs evaluations) But for more advanced cases you could use something like Genetic Programming with Koza's Automatically Defined Functions where you build an intermediate library of useful blocks. Now one would use deep learning and produce source code directly with some tool like Copilot and run it until it passes all tests. Or if you want to get your hands dirty, you can re-implement the old school methods and use a neural network to make the pick decisions instead of a random pick. Once you have programs that pass all test cases, you can try to prove correctness (that's more something like HOL-Light would do) and whether or not they are equivalent (and equivalent to a formal specification) and optimize them further by transforming the program.
- aasasd 5y ago
  Interesting, thanks!