Sukyoung Ryu - Programming Language Research for Technical and Social Good (KAIST)

Developing mechanized specifications for JavaScript, WebAssembly, and P4. This is what I meant by Metaprogramming and it works. This project was funded by the Korean Government. I wish I could pay them my income tax.

 

See https://wasm-dsl.github.io/spectec/ and https://github.com/es-meta/esmeta.

Jihyeok Park - Trusted JavaScript Language Environments with ESMeta. See https://github.com/es-meta/esmeta

 

Xiaohong Chen - Programming Languages Must Have Formal Semantics. Period. See https://kframework.org/

The panel discussion on Real-World Programming Languages

The Rust guy goes on and on and on. Definitely too much 'real-world' there. The problem is a huge chunk of what some people call the real world is just what Edsger W. Dijkstra called "Getting lost in complexities of your own making" and a lot of the real world just isn't in the purview of programming language and operating system designers at all because it is completely and utterly beyond reach. I mean the stuff I mentioned in Programming Paradigms, but also how organisations can effectively use computer communications without needing to employ 'experts' to write and maintain buggy code full of security vulnerabilities. There is a nice example of such an application at 22:23 what they are able to do is specify an application domain (hospital admissions system) formally and generate software and documentation which, at least in principle, could be formally formally verified against that. To see the significance of this discussion it helps to know P4 targets hardware like https://netfpga.org/.

Subscribe to ACM SIGPLAN.

Comments

Post a Comment

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Image
A derivative is linearisation, and differential calculus is essentially linear algebra, ...  See  Freya Holmér - Why Can't You Multiply Vectors?  and  Freya Holmér on Continuity of Splines . See also the MIT OCW page:  Matrix Calculus For Machine Learning And Beyond  (Alan Edelman, Steven G. Johnson) Subscribe to The Julia Programming Language . Alan Edelman talking about expressing mathematics as computer code. The idea is that you can use computer languages to communicate mathematical ideas precisely to other people. See my comments about functional programming languages here:  https://prooftoys.org/ian-grant/hm/ Subscribe to TEDx Talks .
Read more

How Could One Unify CMU and MIT

Image
I mean, how to get the best of the two different philosophies of computation. One is based on typed programming languages and the other on engineering with diagrams . This is about practical computing and the cost and feasibility of software development in general. Here is the problem: We have a lot of algorithms which can all be described abstractly using some sort of pseudocode, or perhaps using some particular language (usually Python!). These algorithms are often well-studied and a lot is known about them in terms of their computational complexity in time and space. Substantive practical software systems invariably employ many such algorithms, often implemented in libraries with more or less well-specified APIs. But very few of these libraries are capable of interoperating because they are either packages written in some specific programming language like Java or Haskell, say, or they are written in C and used as object code, or they are written in an interpreted language like Sc...
Read more

Tensor Fields and Simplicial Complexes

Image
Listening to Freya Holmér last night I started to get glimmers of an idea I had long ago about how to represent vector spaces in computational processes using this recursive abstract type :  abstype 'a point = POINT   of {getx :  'a vector,       diff :  'a point -> 'a point,       move :  'a point -> 'a point,       scale : 'a -> 'a point,       proj :  'a point -> 'a} with    fun new i (op +) (op -) (op * ) dot =    let fun self x =  POINT       {getx = x,        move = fn (POINT pr) =>           (self (x + (#getx pr))),        diff = fn (POINT pr) =>          self (x - (#getx pr)),        scale = fn i =>          (self (x * i)),        proj = fn (POINT pr) =>     ...
Read more