i feel that the grammar of a programming language is among the least appropriate of all possible facets of its behavior to start off with.

[hipsterelectron@circumstances.run]

In practice, ML implementations may provide a directive as a form of top-level declaration for including programs from files rather than directly from the terminal.

FILES??? TERMINAL????

[hipsterelectron@circumstances.run]

So far, for simplicity, we have used the same notation B to stand for both a static and a dynamic basis, and this has been possible because we have never needed to discuss static and dynamic semantics at the same time.

i understood compilation to be the translation from an IR (static semantics) into the ABI (dynamic semantics)

[hipsterelectron@circumstances.run]

C Appendix: The Initial Static Basis
In this appendix (and the next) we define a minimal initial basis for execution. Richer bases may be provided by libraries.

for "execution" means something different to the authors than it does to me

[hipsterelectron@circumstances.run]

omg

At the same time, imperative features were important for practical reasons; no-one had experience of large useful programs written
in a pure functional style. In particular, an exception-raising mechanism was highly desirable for the natural presentation of tactics.

these are still a matter of grammar to me. "imperative features" is an interface to the programmer imho

[hipsterelectron@circumstances.run]

The full definition of this first version of ML was included in a book [19] which describes LCF, the proof system which ML was designed to support.

literally omfg why didn't you send me there FIRST?????

[hipsterelectron@circumstances.run]

Other early influences were the applicative languages already in use in Artificial Intelligence.

i am not the expected audience

[hipsterelectron@circumstances.run]

i keep reading to find when i'm gonna find some discussion of semantics. hasn't happened yet

[somebody@tech.lgbt]

@hipsterelectron they hated it when Margaret Hamilton wrote AXES001 entirely about semantics thereby actually inventing software engineering without getting credit. those kinds of men are allergic to reflection

[hipsterelectron@circumstances.run]

@somebody it's so incredibly obnoxious. pages upon pages telling the deeds of great men

[hipsterelectron@circumstances.run]

the reason i fell into this trap in the first place because i wanted to understand what "C formalized in HOL" was on about https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-453.pdf

C also combines a number of interesting features on the theoretical front, making it additionally interesting as a subject of study.

this is not something i wanna hear from someone claiming to have formalized it

For example, C’s expressions both are side-effecting and have very under-specified evaluation orders. If these semantic features were the main area of interest in studying a language, then it would clearly be easier to construct a simple calculus that included these features and little else.

this is ridiculous. obviously these semantic features are not ideal when attempting to write code that runs e.g. in ring 0. yet people do it (and this is meaningfully outside the C standard). the UB becomes defined thanks to our friends who write the compiler. is it worth attempting to standardize ring 0 properties?

However, we prefer to attack as much of C as possible all at once. As Milner and Tofte point out in the commentary on the definition of SML [MT90], this study of languages in their entirety has its own grounds for interest, and we further feel that our study of C gives us a possible
application in the area of software verification.

they didn't even mention a single concrete implementation until the appendices

[hipsterelectron@circumstances.run]

This style of definition was used in the definition of Standard ML by Milner, Tofte and Harper [MTH90]. This example, one of the most famous formal language definitions, is a clear demonstration that a large language can be formalised in this manner.

i'm getting the impression that the seL4 HOL C semantics may not be as useful as it's being let on lmao

[hipsterelectron@circumstances.run]

Precisely because the standard’s definition of C is not formal, we can never hope to prove our formal definition consistent with it.

actively violent and evil thing to say

[hipsterelectron@circumstances.run]

At best we can hope that our definition comes to be seen as correct by the community of people concerned with C’s definition and standardisation.

this is now becoming kind of worrying. a formal semantics can be matched to the behavior from a compiler and our friends in the compiler and in our CPU architecture manuals can describe whether it matches the "formalization"

Such a community can perform very useful error-checking.

how does anyone write this stuff

[hipsterelectron@circumstances.run]

In addition, if used as the basis for software tools that do not necessarily require a deep understanding of its details, a formal semantics may come to be accepted as correct simply because of what it has made possible in the pragmatic domain.

this is FUCKED! a formal semantics is not something you can bully people into accepting. jfc

[hipsterelectron@circumstances.run]

A denotational semantics defines an appropriate mathematical space as a model for a language, and maps the language’s syntax into that space in a way that is compositional. This property requires that the semantics of a syntactic phrase be a function of the semantics of the phrase’s syntactic sub-components.

so "denotation semantics" is a made up interpretation that conforms to some fuckboy's idea of aesthetically pleasing. see i'm learning so much

[hipsterelectron@circumstances.run]

it keeps going. now he's claiming to be the first to have invented the C abstract machine (operational semantics)

[hipsterelectron@circumstances.run]

OMG

It is central to our thesis that the semantics of C is so complicated that it can only be usefully manipulated in the context of a theorem prover.

THE C STANDARD IS WRITTEN BY HUMANS? FOR HUMANS?

[milo@types.pl]

@hipsterelectron im on team operational semantics

[hipsterelectron@circumstances.run]

this is also pretty worrying because he dismissed earlier ever conforming with the C standard, and seL4 literally just asserts that its C code conforms to the model

[hipsterelectron@circumstances.run]

like this was not some newfangled thing people started doing recently! people writing code that needs to validate nontrivial properties generally do it by actually getting their hands dirty and doing the work to link the compiler's internal semantics to the representation made in HOL or whatever