Will JDK always be required?

[erlend-sh]

The model checker requires Java Development Kit

Any plans to change this?

You probably have perfectly valid reasons to use Java in the Quint stack (something to do with upstream TLA tooling I presume), but I know a lot of (young) developers who will instinctively go looking elsewhere when the JDK is part of the development workflow, so I just wanted to get your thoughts on this.

[bugarela]

This is the first time I heard of this reservation 😅

There is generally an effort in the TLA+ community to make the tools available in a web version with WebAssembly. If we ever manage to make Apalache work with wasm, then that might be a path for avoiding the JDK dependency - but there are no current efforts towards that.

It's possible to use a lot of Quint features without JDK tho. It is only needed for the quint verify command, which is usually the last command to be used by new users. So I guess this gives people the opportunity to try Quint without this extra installation step and then only have to go through it if they actually like the language and want to use verification.

[aumetra]

Interesting! Also I saw that Apalache is written in Scala. Have there been attempts to translate its bytecode via TeaVM into Wasm?
I mean, I'm not sure how viable it is all in all.

[erlend-sh]

Cheers 😊 I know it’s a rather silly concern but it came up in conversation with some folks who are evaluating Quint so I figured I may as well raise it for posterity.

[zicklag]

Yeah, I tend to have a bad experience when needing to use Java-based tooling, but I think a lot of it's a culture thing, or else just less modern standards. And the fact that Oracle was being weird and not allowing cool Open JRE implementations like OpenJ9 to publish built binaries.

It's semi personal preference, but also supported by real difficulty when I have to use Java-based software, which is probably aggravated by me developing behind an HTTP proxy that Java tends not to work with.

Anyway, I really like the modern take of quint so far. I'm really excited about it. 😄

I've wanted to learn TLA+ for years, and just started learning it in the last month, but I really appreciate the ease of use and modern workflow of Quint.

Also Apalache does look like a pretty solid project from first glance. Maybe one day I'll find a way to write a Rust solver backend. 😁

[bugarela]

Have there been attempts to translate its bytecode via TeaVM into Wasm?

I don't think so. I know there are some blockers into translating it to wasm (due to some libraries iirc), but I don't really know what was attempted there. This might be a good question to ask in https://github.com/apalache-mc/apalache/