Languages

Top Wonderings

  • What we can do to enable everyone writing a new OS kernel as easily as a user applications?

    • What is the difference between applications and OS kernels? Is kernel just a special application?
    • A new language designed for easy coding for OS kernels, just as other domain specific languages?

  • A single application written using a mix of different languages and how can we securely compile/link them together without sacrafices the security properties of each language?

  • How to capture all the side effects of C functions and effectively turn it into a functional-like language where all side effects are made explicitly made as ‘returned value’.

    • so that we can make formal verification of C as easy as in Haskell, Ocaml, etc.
    • C–?
  • Closure

    • Reference 1 reference ↩

  • Lambda

    • Reference 1 Lambda: Syntactically, lambda refers to a form for describing anonymous functions. But a lambda does not become a function pointer. It becomes a closure. Closures are data structures with both a code and a data component. Two strategies to compile lambdas into closures: Flat closures Linked (or shared) Closures Closure Conversion: flat closure is top-down compilation; and linked(or shared) closure is bottom-up compilation. Lambda Lifting Reference [^wiki-lambda-lifting] 1982 by Thomas Johnsson.

  • Langs

    • Reference 1 Sequoia Reference 1 http://web.stanford.edu/group/sequoia/ http://web.stanford.edu/group/sequoia/cgi-bin/ reference ↩ C & C++ Reference 1 Copy Elision when return a struct. Mesh: Fragmentation in C/C++ Reference 1 MESH: Compacting Memory Management for C/C++ Applications, PLDI, 2019. ↩ reference ↩ NesC Reference: Go Reference: Concurrency Setup Environment Variables Reference: GOPATH: environment variable that specifies the location of your workspace. If no GOPATH is set, it is assumed to be $HOME/go on Unix systems and %USERPROFILE%\go on Windows.

  • Tensors

    • Reference 1 Why tensor? What is a tensor? From datacamp: Vectors: ordered collection of numbers; one column matrices; a scalar magnitudes that have been given a direction, where direction is relative to the reference direction. Vector space: two-space: (x,y); three space (x,y,z); Unit Vectors: $\hat x$, a magnitude of one. Tensor: a mathematical representation of a physical entity that may be characterized by magnitude and multiple directions.

  • Mix Langs

    • Reference 1 FunTal Reference 1 FunTAL: Reasonably Mixing a Functional Language with Assembly ↩ All the languages together ↩

  • Tapl

    • Reference 1 Semantic Style Semantic Styles (chapter 3.4 in 1) There are three basic approaches to formalizing semantics: Operational semantics. Specifies the behavior of a programming language by defining a simple abstract machine on it. For simple languages, a state of the machine is just a term, and the machine’s behavior is defined by a transition function that, for each state, either gives the next state by performing a step of simplification on the term or declares that the machine has halted.

  • Aspect Oriented Programming

    • Reference: what is aop

  • Class PLDI

    • Q & A Does functional programming have object oriented programming style? What is essential part for a domain specific language? References: CSC 2⁄454 Programming Language Design and Implementation, by Prof. Micheal Scott Aug 28. names of PLs (IMPERATIVE) C#, C, Swift, Java, Ada, Rust, Pascal, scala, Algol, Go, Obj-C, Fortan, C++, B, PL/I, X, (SCRIPTING) Kotlin, Python, Julia, Javascript, PHP, R, Ruby, small talk, (FUNC) Lisp, Scheme, ML, Haskell, Erlang,

  • Typed Assembly Language

    • Reference1: Statically typed intermediate languages are effective tools for staging the compilation of high-level languages. Types express invariants that help programmers understand their programs, and strongly typed languages prevent many common programming errors. Compiler writers can use these properties to debug sophisticated program transformations such as closure conversion and optimizations like datatype specialization. Furthermore, types not only help check the correctness of transformations but enable analyses or optimizations that are extremely difficult without them.

  • Types

    • Reference 1 Gradual Typing Reference 1 RUST ——–buffer——–> Ocaml <——————— Escape Hatches: ML:C FFI Rust:unsafe Java: JNI All type soundness(safety) guarranttes are gone. Instead, use Principled FFIs: ML: linear types. Linking types: support safe initeroperability with other languages. Only need linking types extensions to interact with behavior/features inexpressible in your language. SNAPL’172: Linking Types for Multi-language Software: Have your cake eat it too. Teach Ocaml with ownership in Rust: Linking Type: linear type: cannot keep it and give it away at the same time.

Created Jul 30, 2019 // Last Updated Jul 8, 2021

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?