3 ms·

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 s

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.
- doublec 8y ago
  ATS enables declaring the interface to C libraries to a very detailed level for proving. It can make using C libraries more safe than using them from C, once defined. Here is an example I wrote about how to make calling a C library safer from ATS https://bluishcoder.co.nz/2012/08/30/safer-handling-of-c-memory-in-ats.html https://bluishcoder.co.nz/2012/08/30/safer-handling-of-c-mem...
- vmchale 8y ago
  You can declare an API with ATS types that ends up being safer than the C API, so when using the library you have greater safety than a C user.

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.
doublec 8y ago
ATS enables declaring the interface to C libraries to a very detailed level for proving. It can make using C libraries more safe than using them from C, once defined. Here is an example I wrote about how to make calling a C library safer from ATS https://bluishcoder.co.nz/2012/08/30/safer-handling-of-c-memory-in-ats.html https://bluishcoder.co.nz/2012/08/30/safer-handling-of-c-mem...
vmchale 8y ago
You can declare an API with ATS types that ends up being safer than the C API, so when using the library you have greater safety than a C user.