Typed Jessie Progress?

I’ve heard someone was working on making a TypeScript flavor of Jessie. Can anyone get me pointed towards that?

Michael Fig @michaelfig has been doing some work in that area. Is this what you’re looking for?

1 Like

Hi Dan, Kate,

Tessie started at Michael Fig’s message at https://github.com/Agoric/Jessie/issues/27#issuecomment-475120848

See https://github.com/michaelfig/jessica/blob/master/lang/nodejs/tessc.ts

Watch https://youtu.be/4jznlS-3jl4?t=5445

On some thread somewhere, I remember posting Dean’s suggestion that perhaps Tessie, being a translator from a source language that’s a syntactic subset of TypeScript but semantically only (approximately) a fail-stop subset of TypeScript, could also inject dynamic type checks according to the type declarations while still being a fail-stop subset. Perhaps, with this injection, Tessie could be soundly statically typed?

If so, Tessie would fill an important hole in our overall story. We’ve been saying “Use Jessie to write code that can eventually be statically analyzed for safety properties with confidence.” However, people who want that will think to first find a soundly statically typed language.

1 Like

Nevermind the “some thread somewhere”. It is that same thread: https://github.com/Agoric/Jessie/issues/27#issuecomment-475120848

(is a broken link!) Here is the new Babel-based https://github.com/michaelfig/jessica/blob/master/lang/nodejs/tessc.js and https://github.com/michaelfig/jessica/blob/master/lang/nodejs/babel-tessie.js.

I found the Typescript Compiler API to be extremely difficult to use for the sorts of rewrites I was trying to do with tessc.ts. So, I kept using tsc for the typechecking, but switched to Babel to do the rewrites.

Tonight I parsed the entire Jessica library sources with Jessica, and have validated that my Tessie sources (lib/*.mjs.ts) are rewritten as valid Jessie by tessc.js with the syntactic restrictions I’ve proposed in the immunize() discussion.

These sources (lib/*.mjs) have been published to Jessica’s master branch.

As for sound typing of Tessie, that’s an open question. Sound typing of the AST data structures themselves is a real challenge… Typescript’s inference doesn’t do well with Arrays-as-tuples, and Typescript always allows you to punt to the void *-equivalent any.

2 Likes

Hi @michaelfig,

Hi Michael, could you provide some documentation on how to use these files? Can I plug them into babel and turn some TypeScript into Jessie? Ideally they’d be published to npm for easy installation in a project, I’m willing to help package that with some guidance.

Splitting Jessica into separate packages is one of my upcoming goals (I want to package the PEG library separately). Unfortunately, tessc.js applies some experimental rewrites that should be omitted.

A proper Tessie package would strip the type information, ensuring use of unknown instead of any and enforce the absence of most globals (as Jessica’s typings specify). Rewites can come later.

If you npm install in Jessica/lang/nodejs, then you can run tessc.js on each .js.ts file.

Feel free to follow up in Github issues, at https://github.com/Agoric/jessica

1 Like

I did look into stripping type annotations, maybe the limited grammar here lends to a more tenable first approximation… Side note, I draw the line on anything TSX/JSX related (on principle)