Hacker Newsnew | past | comments | ask | show | jobs | submit | azdavis's commentslogin

I wrote a small post on that: https://azdavis.net/posts/lambda-cube/

Hope it’s helpful!


Cool that you worked on an implementation of the CoC.

I've been somewhat wanting to go back and revisit ATAPL and read chapter 2 on this subject: https://www.cis.upenn.edu/~bcpierce/attapl/frontmatter.pdf


That is a good post. I've linked to it from mine!


Thanks! But I don’t think it quite worked?


Ought to be fixed now


This is likely in response to https://news.ycombinator.com/item?id=43863937


I didn’t realize that “docs like code” was a noun phrase and was trying to figure out how docs can be liking code that is in basic terms.


Even without that particular misunderstanding I found it very hard to initially parse what this was actually about; I'm skeptical that a naïve non-technical person will be able to work out what it's banging on about. Maybe they're expected to arrive from some other origin with a bit more context?

To me "Docs like code" conjures up documentation that looks like code, so I think something like "The basics of using programmers' tools to create documentation" would be clearer.


Thanks for pointing this out. The post starts from the assumption that people have at least heard of "docs like code", because it's a widely-used term/practice in tech writing. So I was aiming at tech writers who heard the term, but lacked the knowledge to use the technique (original draft of the post was in response to a less technical tech writer asking me a ton of questions)

But perhaps I need to explain this up top, rather than hoping people will hang in there until the explanatory section.


> it's a widely-used term/practice in tech writing

But it's not. You have got the key phrase wrong!

It's Docs as Code.

There are whole websites devoted to it:

https://docsascode.org/

Not "like": As -- meaning, "create docs as you create code", meaning "using the same tools and methods."

There is a good strong evidence that your version is inferior: the dozens of comments in this thread by people baffled by the phrase, or pointing out its flawed construction.

It's the Docs As Code approach, _NOT_ "docs like code".

https://docascod.github.io/howto/#/

https://marketplace.visualstudio.com/items?itemName=rafaelmn...

https://www.synesthesia.co.uk/tag/docsascode/


Yup, Docs as Code is the more well-known phrase.

https://www.writethedocs.org/guide/ See

Approaches to creating documentation Docs as Code Docs as Code at Write the Docs Docs as Code at other conferences, video casts and articles DocOps What is DocOps, anyway? Who practices DocOps? DocOps resources


This really depends on where you first encountered the term. Anne Gentle wrote Docs Like Code, the first book I read on this topic 8 years ago. I always consider the terms "docs as code" and "docs like code" to be interchangeable, and usually use both when discussing the topic with an audience that includes a wide variety of different individuals. I think "docs as code" is probably used more in purely dev circles due to the proliferation of the "everything-as-code" construction seen in other dev-adjacent disciplines (infra-as-code, config-as-code, etc.)


FWIW, I was first taught this approach at Red Hat in 2014. I think DaC has precedence and I've never, ever encountered DlC in my work in half a dozen companies in 4 or 5 countries.

I am not saying you're wrong. I'm merely reporting my own experience.


time flies like an arrow


And fruit flies like a banana


docs is plural. You can't have a plural in a noun phrase, other than in he head position.

For instance

OK, no plurals: law school entrance test

OK, head plural: law school entrance tests

?? non-head plural: law school entrances test


Interesting. Can you provide some source(s) for this rule?


The source is the English language, do you speak it? :)

Nouns that appear as modifiers in a compound noun are singular, and the need for a singular is so strong that English speakers invent singulars forms of plurale tantum words such as "jean jacket" rather than "jeans jacket".

There are certain cases in which a plural modifier cannot be avoided, mainly because a plurale tantum doesn't singularize. We cannot singularize "goods" in "goods distribution network"; if we drop the "s", we get an adjective which completely changes the meaning.

However, consider the word "supplies" which normally doesn't go to the singular word "supply" denoting one item. Yet in business we have "supply chain", not "supplies chain".

There is a strong urge to eliminate plurals from the non-head position of a compound noun; the urge only loses in cases when a special kind of plural cannot be eliminated.


Especially since people like to play fast and loose with things like plurals in set phrases.

See eg https://www.youtube.com/watch?v=AxlzkJAK1BM&t=22s


"Docs" is short for "documentation", not "documentations".


It's kind of its own thing at this point, people write "design doc" in singular so "docs" could very well be short for "documents".


Bingo - it’s colloquially



"Docs" is short for "documents". It is widely understood to also stand for "documentation", but AFAIK even in that use, grammatically it still behaves as if it stood for "documents".


Even docs is understood as a plurale tantum noun like scissors, it still cannot be in a non-head position in a noun phrase.

If we make a noun phrase in which scissors is embedded as a non-head position, we take out the s.

We want to hear "scissor sharpening service", rather than "scissors sharpening service".

The latter is not considered grammatically incorrect, but it lacks euphony.

In some cases plural-sounding words can't be avoided in the middle of noun phrases, like "denotational semantics lecture". Semantics is a singular that people treat as a plural sometimes ("these semantics are ..."). We can't delete the "s" to make semantic, because then we get an adjective. That can be in the middle of the noun phrase, but it changes the semantics. A semantic lecture isn't one about semantics but one that has semantics (about any topic whatsoever).


"law schools enter test"


I'm not sure what argument you're trying to make there; but you no longer have a four-word noun phrase here. It reads like [S law schools] [V enter] [O test].


In "docs like code" the first noun is plural. Your examples were pluralising other words.


Yes: the first position isn't special; the last is. The head of a compound noun in English is the last word. The thing denoted by A B C D is a D, first and foremost. The nouns A B C are modifiers applied to D, in the order C B A. They normally cannot be plurals.

Even when a plurate tantum such as "scissors" is used as a modifier in the non-head position, English speakers invent a singular form for it, giving rise to usage like "scissor blade".

The 1990 movie starring Johnny Depp could not have been called Edward Scissorshands.

(I would go as far as to suggest that "scissors blade", though widely used also, is a hypercorrection based on the forced idea that there is no "scissor".)


Might this help? I wrote it: https://azdavis.net/posts/define-pl-01/


SML pops up now and again on HN, which is always nice to see. I wrote a language server for SML in an attempt to improve the tooling situation around the language: https://azdavis.net/posts/millet/

The main motivator for why I did this is because we use SML as a teaching language at my university and students always seem to struggle with the error messages and tooling from the compiler.


I made a language server for SML with a focus on attempting to provide good error messages: https://azdavis.net/posts/millet/


it's wonderful and thank you :)


Glad to see new languages designed around having good support for IDEs. matklad (rust analyzer) and I wrote a bit about this:

- https://matklad.github.io/2023/08/01/on-modularity-of-lexica...

- https://azdavis.net/posts/pl-idea-tooling/

I think pure functions, sum/product types, and pattern matching are generally accepted as an excellent way to model and manipulate pure data. I wonder what the team’s thoughts are about handling less pure things like asynchrony and I/O, as well as more interesting control flow like exceptions/panicking, coroutines, generators, iterators, etc.


For the IDE use case, I made a language server for SML: https://azdavis.net/posts/millet/


For editor support for Standard ML you can try Millet, a language server. https://azdavis.net/posts/millet/

There’s also https://smlhelp.github.io/book/ which is mostly put together by current/past CMU students.

Note: I made Millet.


I’ve been working on a language server for Standard ML called Millet: https://azdavis.net/posts/millet/

There was some past discussion about it on HN: https://news.ycombinator.com/item?id=32512715

For my part, I think it’s unfortunate that virtually no mainstream language has a formal semantics in the style of SML’s Definition. I wrote a bit about formal programming language semantics in a series of posts: https://azdavis.net/posts/define-pl-01/


I've had a quick look over your posts, and I will look over the more carefully as a refresher on these kinds of things (I have looked at Hoare logic which this resembles, and a couple of other related things). The problem is to me, the formal semantics aren't actually very different from what you would write in English, and the real problem, and this is never addressed, how do I use this (which includes: how do I manipulate these things symbolically to some useful end)? The reason I don't get more deeply stuck into these formal semantics is because they seem to have no way for me to actually do anything useful with them. This lack of a 'bridge' is a huge problem to me because I can't justify learning that which appears of no use.

Any comments appreciated, and don't be put off by the negative tone of this, it's just frustration.


The biggest reason why you'd want a formal semantics for your PL, as opposed to just a "human" language specification, is so that you can do proofs about the formal semantics. You can prove your PL, as defined, satisfies certain "safety" properties. And the point of doing these proofs is is to check that the definition of the PL "makes sense".

PLs that don't have a formal semantics (aka, most mainstream PLs) are more likely to be in situations where implementors realize, after the standard has been written, that e.g. some of the PL's features interact in a way that doesn't make sense, such as this example with C++ coroutines and lambdas: https://news.ycombinator.com/item?id=33084431

Two of the most common safety properties of interest are progress and preservation. (I touched on this in the last above linked post near the bottom.) At a high level:

1. Progress states that if you have a program that type-checks, then either that program is "done" or it can continue evaluating.

2. Preservation states that if you have a program that type-checks and that can continue evaluating, then as it continues to evaluate, it continues to type-check.

Note that the conclusion of preservation "feeds back" into progress: the program type-checks. And vice versa: progress may state as its conclusion that the program can continue evaluating, which then lets you apply preservation. This means you can keep applying the progress and preservation theorems in a "loop" until the program is done evaluating.

For each of the 4 posts in my series about formal semantics, I duly translated the rules presented in the blog post into Lean code, and then proved that the rules do satisfy the safety properties. For example, for the first post linked above:

- The syntax of the language: https://github.com/azdavis/hatsugen/blob/part-01/src/syntax....

- The static semantics (the "typechecker"): https://github.com/azdavis/hatsugen/blob/part-01/src/statics...

- The dynamic semantics (the "runtime"): https://github.com/azdavis/hatsugen/blob/part-01/src/dynamic...

- The proofs of safety: https://github.com/azdavis/hatsugen/blob/part-01/src/safety....


I have a background in formal methods and PLs, and never used it. I understand the supposed benefits but IME they never got used.

Clearly you have used it, so I'll take time looking over your stuff (though I don't know lean).

I appreciate you taking the time to write a comprehensive answer, as I said, I'll try to do it justice!


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: