It would be fabulous to see an update after oh these many moons: How much success did the project see? Where is it used? Have the standards bodies figured out about toolchain integrity?
6:21 Lean4 extracts C programs although the extraction process doesn't seem to have been formally verified. There is also ATS-lang that builds proofs around existing C code.
Dependent types are the complex numbers of type theory. They fill a gap previously present, and is archaic enough that the layman will probably never interact with it
25:2025:54 if bugs come at big price (loss) - language with more (longer) typing (enforced correctness) needed. if bugs are costless (or acceptable) - language with less typing will do the job much quicker.
If a program loads an ECU such that the ECU draws too much current, the PSU voltage drops and a driver alert doesn't sound then would this fall under the problem of operational semantics in the same way as the example that deletes the filesystem? If so then, given people never seem to give load and memory activity/occupancy any consideration with denotational semantics, how are denotational and operational semantics different? Is it just a question of awareness? IE, if you are aware there are files and they can be absent then to consider them is denotational semantics and to ignore them wilfully is operational semantics - but if you're not aware then it's all denotational semantics?
Operational and denotational semantics are just different abstractions with the same end-goal: make it possible to formally verify your (non-trivial) program. It's just that certain language or hardware features are more-or-less awkward to model, and hence more or less likely to contribute to the semantic gap that the speaker is trying to minimize. TL; DR, there's (still) no holy grail, though things are (slowly) improving. The two approaches each lend themselves to different kind of systems, and you still can't have your cake and eat it too.
Eventually these lines of research will start to converge, and some deep results will show what the trade-offs are in a precise way. But until then, you have to try to wrap your head around all of it, and try to choose the best approach for the work you're doing. And yes, that as horrible as it sounds.
Didn't they already solved this problem with sel4 kernel? It has been fully proved, but written in C, not rust. Then auto translated into Isabelle /HOL.
It would be fabulous to see an update after oh these many moons: How much success did the project see? Where is it used? Have the standards bodies figured out about toolchain integrity?
It would be nice to hear the questions =)
6:21 Lean4 extracts C programs although the extraction process doesn't seem to have been formally verified. There is also ATS-lang that builds proofs around existing C code.
Dependent types are the complex numbers of type theory.
They fill a gap previously present, and is archaic enough that the layman will probably never interact with it
25:20 25:54
if bugs come at big price (loss) - language with more (longer) typing (enforced correctness) needed.
if bugs are costless (or acceptable) - language with less typing will do the job much quicker.
If a program loads an ECU such that the ECU draws too much current, the PSU voltage drops and a driver alert doesn't sound then would this fall under the problem of operational semantics in the same way as the example that deletes the filesystem? If so then, given people never seem to give load and memory activity/occupancy any consideration with denotational semantics, how are denotational and operational semantics different? Is it just a question of awareness? IE, if you are aware there are files and they can be absent then to consider them is denotational semantics and to ignore them wilfully is operational semantics - but if you're not aware then it's all denotational semantics?
Operational and denotational semantics are just different abstractions with the same end-goal: make it possible to formally verify your (non-trivial) program. It's just that certain language or hardware features are more-or-less awkward to model, and hence more or less likely to contribute to the semantic gap that the speaker is trying to minimize. TL; DR, there's (still) no holy grail, though things are (slowly) improving. The two approaches each lend themselves to different kind of systems, and you still can't have your cake and eat it too.
Eventually these lines of research will start to converge, and some deep results will show what the trade-offs are in a precise way. But until then, you have to try to wrap your head around all of it, and try to choose the best approach for the work you're doing. And yes, that as horrible as it sounds.
Didn't they already solved this problem with sel4 kernel?
It has been fully proved, but written in C, not rust. Then auto translated into Isabelle /HOL.
Well that was incredible
5:00 The proof worked b/c 'lol' happens to be a palindrome. It would have failed on 'haha' :D