black_knight

30 ms·

1. 361.▲
   by black_knight 11y ago

   The claim that the concept of "type" is not formally defined, is rather like saying that the concept of "logic" is not formally defined. In both cases there are several competing, completely formal definitions, each with
2. 362.▲
   by black_knight 11y ago

   I have to disagree to that one needs syntax highlighting and autofilling to be productive in Agda. I have written a fair amount of agda code in Acme, which has neither. Rather I find these bells and whistles distracting — and prefer giving
3. 363.▲
   by black_knight 11y ago

   Emacs is the only officially supported interactive Agda environment, as other people have noted. However, I have written a lot of Agda code in other editors (acme and vim). It is certainly feasable to do! In fact I find that it improves my
4. 364.▲
   by black_knight 12y ago

   While software architecture certainly is an art, I would not say it is unique in that aspect among the fields you mentioned. Both engineering and maths should be considered art in their own rights. If you consider abstract mathematics, it i
5. 365.▲
   by black_knight 12y ago

   I have come to favour the Acme[1] approach of having a virtual file system to interact with the editor, so that you can write compatible scripts in any language! [1] http://research.swtch.com/acme
6. 366.▲
   by black_knight 12y ago

   Yes. It sounds very much like you want to checkout Acme (and Plan 9). You can test Acme on other operating systems to get an idea. On Linux (or Mac I think), you can even mount the file system using fuse, or access it using a special progra
7. 367.▲
   by black_knight 12y ago

   What I find most amazing is how the kernel is more like a file system multiplexer. Its job is to present a file system to each process built from mounting virtual file systems from all sorts of programs and remote machines. If I want to acc
8. 368.▲
   by black_knight 12y ago

   Not quite true. The command "" (much like bash's !!) runs the previous command you entered. It can also be given a prefix of a command and search the history for this command. See wintext(1).