4 ms·

It's interesting to me to see these projects as alt-history, and see them as the dead-end technical choice that they were. Has any programming language since t

It's interesting to me to see these projects as alt-history, and see them as the dead-end technical choice that they were. Has any programming language since then tried to use more than ASCII for its keywords?

AceJohnny2 6y ago
Obviously it belies a very anglo-centric view of the computer engineering landscape, but frankly I think that's a good thing, as it allows easier exchange.
ColanR 6y ago
Mathematica does this, and they solve the keyboard problem with floating palettes of symbols.
- kmill 6y ago
  They also have ESC symbolname ESC, with autocomplete.
jonjacky 6y ago
The Z ("zed") notation -- but that is a non-executable specification language: https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation
gnulinux 6y ago
I program in Agda pretty often and community usually uses Unicode characters for most things, so I do too. The impl of AVL trees in stdlib: https://github.com/agda/agda-stdlib/blob/master/src/Data/Tree/AVL.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Tre... Some basic properties of natural numbers: https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Properties.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat... It makes the code look absolutely gorgeous, readable and it's very easy to type too. I use Emacs agda-mode so it just automatically replaces e.g. \r with → or \== with ≡ etc... I don't use Agda for theorem proving, I make real life programs in Agda, I compile them to Haskell and compile with GHC to executables.
- fwip 6y ago
  That's pretty cool. What kind of problems do you find yourself solving with your Agda code? (Or, asked another way, what sort of stuff do your programs do?)
  - gnulinux 6y ago
    Currently my programs parse text. I have a JSON formatter, a lisp formatter. I'm also writing an Agda preprocessor in Agda i.e. parse Agda-like code, process it, print valid Agda code. I use them in my other projects as tooling. Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.
- ColanR 6y ago
  What font do you use for this? It looks weird with my defaults. I once seriously considered trying to build something that included math symbols in the syntax. It's pretty cool to see that I don't have to.
  - gnulinux 6y ago
    Not currently on my computer with that setup but afair I use Inconsolata.
- arthurcolle 6y ago
  Julia also allows Unicode characters, which I think is great for math-heavy programs. I love that about it. I always forget the keybindings for them though.
  - gnulinux 6y ago
    agda-mode in emacs has fallback option for latex like aliases. E.g. \infty gives ∞ or \cdot gives · it's very convenient if you use latex often. Other than that, if you have no clue, M-x describe-char explains you how to produce a character.
brudgers 6y ago
Racket uses λ for “lambda” and it’s pretty common in Racket code.
WorldMaker 6y ago
Haskell's GHC compiler has a tiny UnicodeSyntax extension and some packages that explore the idea further. UnicodeSyntax: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#unicode-syntax https://downloads.haskell.org/~ghc/latest/docs/html/users_gu... Base Library Symbols: http://hackage.haskell.org/package/base-unicode-symbols http://hackage.haskell.org/package/base-unicode-symbols Containers Library Symbols: http://hackage.haskell.org/package/containers-unicode-symbols http://hackage.haskell.org/package/containers-unicode-symbol...
chc4 6y ago
Urbit's programming language Hoon uses two character "runes" instead of keywords. Here's the standard library and compiler source, for example: https://github.com/urbit/urbit/blob/master/pkg/arvo/sys/hoon.hoon https://github.com/urbit/urbit/blob/master/pkg/arvo/sys/hoon... There's a full rune reference available at https://urbit.org/docs/reference/hoon-expressions/rune/ https://urbit.org/docs/reference/hoon-expressions/rune/, but tldr they're group into families, with the first character being broadly what it does. AST nodes that have to do with "conditionals" are ?:, ?., ?@, etc. I don't think anyone uses non-ASCII diagraph fonts for them, but it wouldn't be a big jump.

AceJohnny2 6y ago

Obviously it belies a very anglo-centric view of the computer engineering landscape, but frankly I think that's a good thing, as it allows easier exchange.

ColanR 6y ago

Mathematica does this, and they solve the keyboard problem with floating palettes of symbols.

kmill 6y ago
They also have ESC symbolname ESC, with autocomplete.

jonjacky 6y ago

The Z ("zed") notation -- but that is a non-executable specification language: https://en.wikipedia.org/wiki/Z_notation https://en.wikipedia.org/wiki/Z_notation

gnulinux 6y ago

I program in Agda pretty often and community usually uses Unicode characters for most things, so I do too. The impl of AVL trees in stdlib: https://github.com/agda/agda-stdlib/blob/master/src/Data/Tree/AVL.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Tre... Some basic properties of natural numbers: https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat/Properties.agda https://github.com/agda/agda-stdlib/blob/master/src/Data/Nat... It makes the code look absolutely gorgeous, readable and it's very easy to type too. I use Emacs agda-mode so it just automatically replaces e.g. \r with → or \== with ≡ etc... I don't use Agda for theorem proving, I make real life programs in Agda, I compile them to Haskell and compile with GHC to executables.

fwip 6y ago
That's pretty cool. What kind of problems do you find yourself solving with your Agda code? (Or, asked another way, what sort of stuff do your programs do?)
- gnulinux 6y ago
  Currently my programs parse text. I have a JSON formatter, a lisp formatter. I'm also writing an Agda preprocessor in Agda i.e. parse Agda-like code, process it, print valid Agda code. I use them in my other projects as tooling. Using Sized Types you can do pretty much anything in Agda though. It's not technically Turing complete since all programs are proved to terminate but you can go very far with it. I really like it because it gives very robust guarantees which makes it very easy think about the state of your program.
ColanR 6y ago
What font do you use for this? It looks weird with my defaults. I once seriously considered trying to build something that included math symbols in the syntax. It's pretty cool to see that I don't have to.
- gnulinux 6y ago
  Not currently on my computer with that setup but afair I use Inconsolata.
arthurcolle 6y ago
Julia also allows Unicode characters, which I think is great for math-heavy programs. I love that about it. I always forget the keybindings for them though.
- gnulinux 6y ago
  agda-mode in emacs has fallback option for latex like aliases. E.g. \infty gives ∞ or \cdot gives · it's very convenient if you use latex often. Other than that, if you have no clue, M-x describe-char explains you how to produce a character.

brudgers 6y ago

Racket uses λ for “lambda” and it’s pretty common in Racket code.

WorldMaker 6y ago

Haskell's GHC compiler has a tiny UnicodeSyntax extension and some packages that explore the idea further. UnicodeSyntax: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#unicode-syntax https://downloads.haskell.org/~ghc/latest/docs/html/users_gu... Base Library Symbols: http://hackage.haskell.org/package/base-unicode-symbols http://hackage.haskell.org/package/base-unicode-symbols Containers Library Symbols: http://hackage.haskell.org/package/containers-unicode-symbols http://hackage.haskell.org/package/containers-unicode-symbol...

chc4 6y ago

Urbit's programming language Hoon uses two character "runes" instead of keywords. Here's the standard library and compiler source, for example: https://github.com/urbit/urbit/blob/master/pkg/arvo/sys/hoon.hoon https://github.com/urbit/urbit/blob/master/pkg/arvo/sys/hoon... There's a full rune reference available at https://urbit.org/docs/reference/hoon-expressions/rune/ https://urbit.org/docs/reference/hoon-expressions/rune/, but tldr they're group into families, with the first character being broadly what it does. AST nodes that have to do with "conditionals" are ?:, ?., ?@, etc. I don't think anyone uses non-ASCII diagraph fonts for them, but it wouldn't be a big jump.