It seems, F* (Microsoft research public domain language addressing specification and verification aspects) is right on the main stream of current programming language evolution/science.
I tried various tags, expecting a tag for this new (meta) language already exists:
- F* (produces all tags with an "f" in it...)
- F-star (does not exist, also produces unrelated google-hits)
- Fstar (does not exist)
I do not seem to have the "create tags" privilege myself yet and even if I had I could not really make up my mind as to what the best tag-name would be for this.
Also, there are a couple of alternate projects going in similar directions (using dependent types and type kinds along with theorem proving technologies to create correct specifications / implementations, some also with code generation facilities for other languages, such as OCaml, F#, JavaScript, etc). Thus, along with the specific tag, maybe someone could come up with a tag summarizing those arising technologies.
Please comment and discuss on the following:
- Create a tag for F*?
- Top level tag - makes sense? What could it be?
For information on the language, see Fstar main web site
f-star