Hacker News Reader

Its unfortunate that ATL is such a generic name. The actual code to which you meant to link is here:

https://github.com/ChezJrk/verified-scheduling

OTOH, a Coq-like DSL written in python would be exciting!

I think it's a reference to APL which is an old, but extremely cool and relevant language and stands for "A Programming Language". APL was all about matrices and vectors too.

Yes, clearly an homage to APL.

Ironically, some (all?) of the same developers appear to be creating a Python DSL based on the work done on the Coq DSL.

https://github.com/ChezJrk/SYS_ATL

Ah it seems that the repos mentioned in this threads are all related after all—

The coq repo is covered by the paper but is a verified version of only the scheduler (a part of the parent python repo, i presume)

Then the repo you linked to seems to be a rewrite/generalization of another(?) lower level part of the main ATL.

Reply on news.ycombinator.com