git @ Cat's Eye Technologies Burro / 2dc2973
Update README and add closing note on TM-to-Kondey translation. Chris Pressey 4 months ago
2 changed file(s) with 31 addition(s) and 43 deletion(s). Raw diff Collapse all Expand all
+25
-43
README.md less more
2525 in the `src` directory, which also serves as the reference implementation
2626 of the language.
2727
28 Note: In some interfaces, viewing the contents of the directory
29 [`src/Language/Burro/`](src/Language/Burro/) will display the contents
30 of this Literate Haskell file nicely formatted as Markdown.
28 Note: In some interfaces (such as Codeberg), viewing the contents of the directory
29 [`src/Language/Burro/`](src/Language/Burro/) will display the definition nicely
30 formatted as Markdown, which is more readable than Literate Haskell.
3131
3232 History
3333 -------
3434
35 ### 2005
36
37 The author, already familiar with brainfuck and starting to learn about
38 group theory and seeing some similarities between them, got some ideas
39 about how they could be combined.
40
41 ### 2007
42
43 Burro language version 1.0 was released. Its documentation
44 can still be found in the file [`doc/burro-1.0.md`](doc/burro-1.0.md).
45
46 ### 2010(?)
47
48 It was noticed and pointed out by ais523 and others that Burro 1.0 programs
49 do not actually form a group.
50
51 ### 2010
52
53 Burro language version 2.0 was designed and released, along with a proof that
54 its programs do form a group, and a proof that the language is Turing-complete.
55
56 ### June 2020
57
58 A more mathematical explanation of the sense in which Burro programs form
59 a group was composed. It can be found in the document
60 [The Sense in which Burro Programs form a Group](doc/The-Sense-in-which-Burro-Programs-form-a-Group.md).
61
62 ### July 2020
63
64 It was noticed and pointed out _(by whom?)_ that the proof of Turing-completeness
65 distributed with Burro 2.0 was incorrect — it only held for very small Turing machines.
66
67 In response to this, a new extensible conditional idiom was developed for Burro code
68 with the aim of writing a correct proof of its Turing-completeness.
69
70 ### 2025
71
72 A minor variant of Burro called Kondey — basically a syntactic sugar for the extensible
73 conditional idiom — was designed, again to support the writing of a new Turing-completeness
74 proof.
35 * **2005**: The author, already familiar with brainfuck and starting to learn
36 about group theory and seeing some similarities between them, gets some ideas
37 about how they could be combined.
38 * **2007**: Burro language version 1.0 is released. Its documentation
39 can still be found in the file [`doc/burro-1.0.md`](doc/burro-1.0.md).
40 * **2010(?)**: It is noticed and pointed out by ais523 and others that the set
41 of Burro 1.0 programs does not actually form a group.
42 * **2010**: Burro language version 2.0 is designed and released, along with a
43 proof that its programs do form a group, and a proof that the language is
44 Turing-complete.
45 * **June 2020**: A more mathematical explanation of the sense in which Burro
46 programs form a group is written up. It can be found in the document
47 [The Sense in which Burro Programs form a Group](doc/The-Sense-in-which-Burro-Programs-form-a-Group.md).
48 * **July 2020**: It is noticed and pointed out _(by whom?)_ that the proof
49 of Turing-completeness distributed with Burro 2.0 is incorrect — it only
50 holds for very small Turing machines.
51 In response to this, a new [extensible conditional idiom](Tests.md) is
52 developed for Burro code, with the aim of supporting a correct proof of
53 its Turing-completeness.
54 * **2025**: A minor variant of Burro called [Kondey](Tests.md) — basically
55 a syntactic sugar for the extensible conditional idiom — is designed,
56 again to support the construction of a new Turing-completeness proof.
+6
-0
Tests.md less more
619619 ...
620620 }
621621 }
622
623 In conclusion, this is the method by which we propose that arbitrary
624 Turing machines could be translated to Kondey, and thence to Burro, thus
625 establishing that Burro is Turing-complete. However, we defer presenting
626 this as an actual Turing-completeness proof until such time as the method
627 can be vetted in a more formal and/or mechanical manner.