5 ms·

Plus for showing code. But I'm a bit confused. Does ATS have a network library? Or a 2d canvas library ? Does it compile to JS !? I would like to see some more

by z3t4 8y ago

Plus for showing code. But I'm a bit confused. Does ATS have a network library? Or a 2d canvas library ? Does it compile to JS !? I would like to see some more real life examples, maybe some simple games like tic tac toe, or a network chat server/client, or what are you supposed to use the langauge for, besides solving fibonacci ?

rurban 8y ago
ATS did beat C++ in the benchmark game. Plus it's a much safer language, with proper contracts and a proper typesystem. It's more comparable to ADA/Spark (just a more C like syntax, not Pascal), than Coq/Agda or any JS based language.
- pjmlp 8y ago
  Actually, the ATS compiler did beat a couple of specific C++ compilers, to be precise.
  - cx101 8y ago
    If it beat g++ and clang++, then it would most likely also beat icc and Visual Studio. The story that icc generates faster code has been a myth for a long time. Or is there another compiler that you have in mind?
    - pjmlp 8y ago
      PGI for example. Many HPC centers happen to believe on the icc myth. Although my point was not to mix languages with implementations.
- gridlockd 8y ago
  > ATS did beat C++ in the benchmark game. It's misleading. ATS is basically a C frontend. If you looked at the ATS implementations in the benchmarks game, it was basically C code. The C implementations usually beat the C++ implementations in the benchmarks game. That's probably why it got removed.
dan-robertson 8y ago
The front page doesn’t do a great job of describing such details. It is a language for systems programming and compiled to fast C. The main idea is that it is supposed to compile to correct C. I’ve no idea if it has a “native” network library. I doubt it has many other libraries but one can call C functions so one can use any library if one wants.
- nine_k 8y ago
  Having to use C libraries for critical stuff like networking (just application-level protocols, like http, not drivers) defeats some of the purpose of provable correctness, etc.
  - cryptonector 8y ago
    Rome isn't built or rebuilt in one day though. Just as in the case of Mozilla with Rust, interoperability with C means there is a path for migrating to a safer world.
  - derefr 8y ago
    I feel like this kind of intensely provably-correct language (this one, Coq, Agda, etc.) isn't so much for writing whole programs in, as for writing the small, very-important-to-verify modules, that will link with other, less important modules to form a whole program. When you're writing provably-correct "error kernels"[1] for your software, you probably want as little interaction with the OS to happen inside the kernel as possible. Write the rest of your program in a glue language, then hand off to the proven-correct error kernel for the hot loop. Probably over stdio, or transactional SHM IPC, or any other mechanism like that that has as little failure-surface as you can get away with. [1] https://medium.com/@jlouis666/error-kernels-9ad991200abd https://medium.com/@jlouis666/error-kernels-9ad991200abd
  - pushpop 8y ago
    It does but without it you have a chicken / egg situation where developers wouldn't use ATS without the library support but those libraries don't get written without developers using ATS. At least this breaks the deadlock and in the future those libraries might be replaced with ATS alternatives.
nine_k 8y ago
Indeed. Quick googling around did not bring me any satisfactory answer. http://www.ats-lang.org/Libraries.html http://www.ats-lang.org/Libraries.html shows that batteries are definitely not included, at least yet.
externalreality 8y ago
I wrote some things a few years ago on ATS. Its introductory but real world: https://www.stackbuilders.com/news/specific-endpoints https://www.stackbuilders.com/news/specific-endpoints. Generally ATS is good for verifying pure algorithms. It has code generators which can compile ATS to C and JS and the like. So if you have a very crucial piece of code and you want to do some formal verification of the process then you can try to use ATS. Other than that its completely a research language. I used ATS to write some stuff for my arduino 5 or so years ago.
- iamcreasy 8y ago
  > Generally ATS is good for verifying pure algorithms. Could you please elaborate on that?
  - externalreality 8y ago
    Yes, "verification" in the formal verification sense of the word. https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification. Also, in ATS the algorithms don't have to be "pure" in the "no stateful side effects" sense of the word to be subjected to verification. ATS is truly a nice piece of master work and hopefully its concepts can start making it out the ivory tower sooner rather than later.
    - iamcreasy 8y ago
      How to do you verify an algorithm? Can you give me an example. Lets say you are trying to come up with some sorting algorithm, and you unknown wrote Bubble sort - how would you go about verifying the algorithm? As far as I know, we test the algorithm analytically and empirically.
      - externalreality 8y ago
        Well, generally, first there has to be some things that you assume to be true - we'll call them axioms (somethings gotta be true, I mean can you prove that the natural number 0 equals the natural number 0). Then you come up with some properties about your algorithm that you want to ensure hold based on those axioms (or stuff already known to be true that are based on those axioms). So, for example, you may want to ensure that your algorithm does not change the length (or more generally the structure) of the input when sorting - e.g. if your sorted list came out with more elements than it went in with that wouldn't be sorting. Now you don't need to have a formal proof for this right away (or at all if you don't want to really). A tool like "Quick Check" (Haskell, Erlang, ...) can help you do a quick informal check by making up a bunch of random list structures and running a unit test on all of them automatically. If your quick check property holds you may want to later try a proof and perhaps even see if something like ATS verification system is expressive enough to encode your proof or prove it for you auto style. The benefit of the verification system is that it happens as static analysis (things that can be determined from reading the code rather than running it) the quick check stuff you need to run the code. A proof is a more complete check. Please read the ATS (Coq, Agda, etc) stuff to learn from the experts.
doublec 8y ago
There are some libraries for ATS, but it's not a well known language so there is not too many out there. ATS makes it easy to mix C by embedding it within ATS, and defining an interface that makes it harder to unsafely use the C API. Since it's so easy most people probably just do this when they need a C library. There are wrappers for libevent which I've used for the network side of long running server side programs in ATS in this manner. With regards to "Does it compile to JS", the answer is yes. There are backends for different languages, JS being one of them. There's also PHP and Erlang backends IIRC.
vmchale 8y ago
> Does ATS have a network library? Or a 2d canvas library ? Does it compile to JS !? I It's pretty easy to use C code for libraries. I haven't use the ATS -> JS compiler myself but I know it exists. Though given that ATS was designed for kernel programming, I'm not sure you'd want to do that. > I would like to see some more real life examples There are some very nice examples, though they tend to be lower-level so things like type-safe channels.

by z3t4 8y ago

rurban 8y ago

ATS did beat C++ in the benchmark game. Plus it's a much safer language, with proper contracts and a proper typesystem. It's more comparable to ADA/Spark (just a more C like syntax, not Pascal), than Coq/Agda or any JS based language.

pjmlp 8y ago
Actually, the ATS compiler did beat a couple of specific C++ compilers, to be precise.
- cx101 8y ago
  If it beat g++ and clang++, then it would most likely also beat icc and Visual Studio. The story that icc generates faster code has been a myth for a long time. Or is there another compiler that you have in mind?
  - pjmlp 8y ago
    PGI for example. Many HPC centers happen to believe on the icc myth. Although my point was not to mix languages with implementations.
gridlockd 8y ago
> ATS did beat C++ in the benchmark game. It's misleading. ATS is basically a C frontend. If you looked at the ATS implementations in the benchmarks game, it was basically C code. The C implementations usually beat the C++ implementations in the benchmarks game. That's probably why it got removed.

dan-robertson 8y ago

The front page doesn’t do a great job of describing such details. It is a language for systems programming and compiled to fast C. The main idea is that it is supposed to compile to correct C. I’ve no idea if it has a “native” network library. I doubt it has many other libraries but one can call C functions so one can use any library if one wants.

nine_k 8y ago
Having to use C libraries for critical stuff like networking (just application-level protocols, like http, not drivers) defeats some of the purpose of provable correctness, etc.
- cryptonector 8y ago
  Rome isn't built or rebuilt in one day though. Just as in the case of Mozilla with Rust, interoperability with C means there is a path for migrating to a safer world.
- derefr 8y ago
  I feel like this kind of intensely provably-correct language (this one, Coq, Agda, etc.) isn't so much for writing whole programs in, as for writing the small, very-important-to-verify modules, that will link with other, less important modules to form a whole program. When you're writing provably-correct "error kernels"[1] for your software, you probably want as little interaction with the OS to happen inside the kernel as possible. Write the rest of your program in a glue language, then hand off to the proven-correct error kernel for the hot loop. Probably over stdio, or transactional SHM IPC, or any other mechanism like that that has as little failure-surface as you can get away with. [1] https://medium.com/@jlouis666/error-kernels-9ad991200abd https://medium.com/@jlouis666/error-kernels-9ad991200abd
- pushpop 8y ago
  It does but without it you have a chicken / egg situation where developers wouldn't use ATS without the library support but those libraries don't get written without developers using ATS. At least this breaks the deadlock and in the future those libraries might be replaced with ATS alternatives.

nine_k 8y ago

Indeed. Quick googling around did not bring me any satisfactory answer. http://www.ats-lang.org/Libraries.html http://www.ats-lang.org/Libraries.html shows that batteries are definitely not included, at least yet.

externalreality 8y ago

I wrote some things a few years ago on ATS. Its introductory but real world: https://www.stackbuilders.com/news/specific-endpoints https://www.stackbuilders.com/news/specific-endpoints. Generally ATS is good for verifying pure algorithms. It has code generators which can compile ATS to C and JS and the like. So if you have a very crucial piece of code and you want to do some formal verification of the process then you can try to use ATS. Other than that its completely a research language. I used ATS to write some stuff for my arduino 5 or so years ago.

iamcreasy 8y ago
> Generally ATS is good for verifying pure algorithms. Could you please elaborate on that?
- externalreality 8y ago
  Yes, "verification" in the formal verification sense of the word. https://en.wikipedia.org/wiki/Formal_verification https://en.wikipedia.org/wiki/Formal_verification. Also, in ATS the algorithms don't have to be "pure" in the "no stateful side effects" sense of the word to be subjected to verification. ATS is truly a nice piece of master work and hopefully its concepts can start making it out the ivory tower sooner rather than later.
  - iamcreasy 8y ago
    How to do you verify an algorithm? Can you give me an example. Lets say you are trying to come up with some sorting algorithm, and you unknown wrote Bubble sort - how would you go about verifying the algorithm? As far as I know, we test the algorithm analytically and empirically.
    - externalreality 8y ago
      Well, generally, first there has to be some things that you assume to be true - we'll call them axioms (somethings gotta be true, I mean can you prove that the natural number 0 equals the natural number 0). Then you come up with some properties about your algorithm that you want to ensure hold based on those axioms (or stuff already known to be true that are based on those axioms). So, for example, you may want to ensure that your algorithm does not change the length (or more generally the structure) of the input when sorting - e.g. if your sorted list came out with more elements than it went in with that wouldn't be sorting. Now you don't need to have a formal proof for this right away (or at all if you don't want to really). A tool like "Quick Check" (Haskell, Erlang, ...) can help you do a quick informal check by making up a bunch of random list structures and running a unit test on all of them automatically. If your quick check property holds you may want to later try a proof and perhaps even see if something like ATS verification system is expressive enough to encode your proof or prove it for you auto style. The benefit of the verification system is that it happens as static analysis (things that can be determined from reading the code rather than running it) the quick check stuff you need to run the code. A proof is a more complete check. Please read the ATS (Coq, Agda, etc) stuff to learn from the experts.

doublec 8y ago

There are some libraries for ATS, but it's not a well known language so there is not too many out there. ATS makes it easy to mix C by embedding it within ATS, and defining an interface that makes it harder to unsafely use the C API. Since it's so easy most people probably just do this when they need a C library. There are wrappers for libevent which I've used for the network side of long running server side programs in ATS in this manner. With regards to "Does it compile to JS", the answer is yes. There are backends for different languages, JS being one of them. There's also PHP and Erlang backends IIRC.

vmchale 8y ago

> Does ATS have a network library? Or a 2d canvas library ? Does it compile to JS !? I It's pretty easy to use C code for libraries. I haven't use the ATS -> JS compiler myself but I know it exists. Though given that ATS was designed for kernel programming, I'm not sure you'd want to do that. > I would like to see some more real life examples There are some very nice examples, though they tend to be lower-level so things like type-safe channels.