Hacker News Reader

Comment by dan-robertson | Hacker News Reader

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.

View on HN

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.

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

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.

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.

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-mem...

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.

Reply on news.ycombinator.com