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.
-
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
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
-
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
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
-
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
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
-
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
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
-
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
it keeps going. now he's claiming to be the first to have invented the C abstract machine (operational semantics)
-
it keeps going. now he's claiming to be the first to have invented the C abstract machine (operational semantics)
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?
-
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 im on team operational semantics
-
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?
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
-
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
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
-
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
Without mechanical support, reasoning with a big semantics is error-prone, and it can be hard to be confident that one’s proofs are actually correct.
does he..........how does he think c compilers work
-
Without mechanical support, reasoning with a big semantics is error-prone, and it can be hard to be confident that one’s proofs are actually correct.
does he..........how does he think c compilers work
Using a theorem prover means that we are confident that all of the results we have proved are correct.
"correct"
Having used the theorem prover HOL [GM93], we are particularly confident, as this system, following the example of its ancestor system LCF [GMW79], uses the strong type system of ML to guarantee that values of type theorem are only produced in ways that are logically sound.
that's it. that's your persuasive essay???
-
Using a theorem prover means that we are confident that all of the results we have proved are correct.
"correct"
Having used the theorem prover HOL [GM93], we are particularly confident, as this system, following the example of its ancestor system LCF [GMW79], uses the strong type system of ML to guarantee that values of type theorem are only produced in ways that are logically sound.
that's it. that's your persuasive essay???
he keeps mentioning like "yeah these theorems take a lot of effort to prove.......and often they're completely unusable too" like sir have you considered that things being difficult might indicate that you need to find a semantics engine that doesn't hate you
-
he keeps mentioning like "yeah these theorems take a lot of effort to prove.......and often they're completely unusable too" like sir have you considered that things being difficult might indicate that you need to find a semantics engine that doesn't hate you
cambridge still batting 100% on being actively evil people who just write whatever they want on official letterhead
-
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?
@hipsterelectron ... if *C* is that complicated, the higher level languages must all be just completely fucked, then, by this standard.
-
cambridge still batting 100% on being actively evil people who just write whatever they want on official letterhead
https://trustworthy.systems/publications/papers/Tuch%3Aphd.pdf
this one is hosted on the seL4 site
Systems impose on languages many abstraction breaking requirements
"systems" lmao
and are not usually considered amenable to implementation in higher-level languages like Java and ML.
yeah cause the JVM abstract machine is specifically built to be this fucked up carnival ride. you could do it if you specifically forked the JVM. hate this lack of precision from ppl who are so loud about "formalism"
For example, zero-copy I/O and address translation are crucial features
zero-copy IO and address translation are extremely different things. zero-copy IO doesn't even make sense in ring 0 and is not in fact a "crucial feature". it's not even a language feature!
and programmers demand the freedom to control data structure layout [87],
you can "control data structure layout" in any language that lets you address bytes which i think is literally all of them. C struct layout is actually rly annoying because you can't let the compiler help you at all
in particular when optimising the cache and TLB footprint that is typically opaque in such languages.
those aren't your data structures those are the CPU's and that's ring 0 again, not a language feature
Inside the research community there are recent promising efforts at harnessing the gains of the last three decades of programming language research [8, 22, 29, 37, 46, 68, 89],
guy who knows nothing about anything he just said: "i represent the 'research community' and we will exterminate your kind"
with an emphasis on types and static checking, when implementing systems.
this guy grew into the rust evangelism strike force
However, these advances are yet to be popularised in industry
guy who thinks "systems" are an industry-specific thing
and still face enormous scepticism from systems implementors who are highly obsessed
with efficiency, sometimes to the extreme where clock cycles are the metric of choice.this fucking guy!!!!! clock cycles can actually be counted reliably lmao. THIS is what seL4 is standing behind
-
https://trustworthy.systems/publications/papers/Tuch%3Aphd.pdf
this one is hosted on the seL4 site
Systems impose on languages many abstraction breaking requirements
"systems" lmao
and are not usually considered amenable to implementation in higher-level languages like Java and ML.
yeah cause the JVM abstract machine is specifically built to be this fucked up carnival ride. you could do it if you specifically forked the JVM. hate this lack of precision from ppl who are so loud about "formalism"
For example, zero-copy I/O and address translation are crucial features
zero-copy IO and address translation are extremely different things. zero-copy IO doesn't even make sense in ring 0 and is not in fact a "crucial feature". it's not even a language feature!
and programmers demand the freedom to control data structure layout [87],
you can "control data structure layout" in any language that lets you address bytes which i think is literally all of them. C struct layout is actually rly annoying because you can't let the compiler help you at all
in particular when optimising the cache and TLB footprint that is typically opaque in such languages.
those aren't your data structures those are the CPU's and that's ring 0 again, not a language feature
Inside the research community there are recent promising efforts at harnessing the gains of the last three decades of programming language research [8, 22, 29, 37, 46, 68, 89],
guy who knows nothing about anything he just said: "i represent the 'research community' and we will exterminate your kind"
with an emphasis on types and static checking, when implementing systems.
this guy grew into the rust evangelism strike force
However, these advances are yet to be popularised in industry
guy who thinks "systems" are an industry-specific thing
and still face enormous scepticism from systems implementors who are highly obsessed
with efficiency, sometimes to the extreme where clock cycles are the metric of choice.this fucking guy!!!!! clock cycles can actually be counted reliably lmao. THIS is what seL4 is standing behind
Even today, it is easy to violate the C type system by its cast mechanism and through address arithmetic.
guy who thinks C's type system is being violated through casting and address arithmetic. you know those have concrete semantics right
The programmer is given, intentionally, access to low-level bit and byte representations of values in memory.
again, that's literally every language
There are no checks on array bounds when indexing — this would violate C’s design philosophy.
the guy who is telling you with a straight face that he totally formalized C semantics for high-assurance ring 0 scenarios is now telling you he finds the language detestable
-
Even today, it is easy to violate the C type system by its cast mechanism and through address arithmetic.
guy who thinks C's type system is being violated through casting and address arithmetic. you know those have concrete semantics right
The programmer is given, intentionally, access to low-level bit and byte representations of values in memory.
again, that's literally every language
There are no checks on array bounds when indexing — this would violate C’s design philosophy.
the guy who is telling you with a straight face that he totally formalized C semantics for high-assurance ring 0 scenarios is now telling you he finds the language detestable
god it would be so cool if rust gave a shit about correctness
-
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 Kind of reminds me of "Proven in Use" defense in automotive, SIL-levels.
Because a certain design has worked for 50 years, it's taken to be correct. Something like that. Now we are down to a few weeks or a product ?
"The requirements of these schemes can be met either by establishing a rigorous development process, or by establishing that the device has sufficient operating history to argue that it has been proven in use."
-
god it would be so cool if rust gave a shit about correctness
C does not have garbage collection and the programmer is responsible for allocation and deallocation of memory through library calls.
"library calls" why would you declare that you don't know the semantics at all
A systems implementor may even develop his or her own memory allocator that replaces this already low-level interface, enabling direct management of the physical memory in a system.
THIS IS THE GUY WHO IS CLAIMING HE KNOWS WHAT SEMANTICS ARE!
-
C does not have garbage collection and the programmer is responsible for allocation and deallocation of memory through library calls.
"library calls" why would you declare that you don't know the semantics at all
A systems implementor may even develop his or her own memory allocator that replaces this already low-level interface, enabling direct management of the physical memory in a system.
THIS IS THE GUY WHO IS CLAIMING HE KNOWS WHAT SEMANTICS ARE!
Unfortunately, systems code is by no means strictly conforming and we could say by definition requires the ability to violate the standard’s strict rules on how memory can be accessed.
i am literally going to go find the C standard right now because the model of globally addressable memory space is i'm pretty sure the one thing that's not violated
