Viewing profile — joomy

A write-up on why I don't give in to the hype and switch to Lean for formal verification of programs.

The issue was a fun read, thanks for sharing.

Our 2 page extended abstract was more like a preannouncement. We hope to have a draft of the full paper by the end of the year. And we're not opposed to choice trees. I personally …

The title alone reads like the "digging for diamonds" meme.

We mean Haskell-style software transactional memory (STM). We call it a primitive because it is not defined in Rocq itself; instead, it is only exposed to the Rocq programmer throu…

I'm not entirely sure I fully agree with this definition; it seems somewhat arbitrary to me. Where is this definition from? My usual intuition is whether the generated code at the …

> Have you considered combinatorial testing? Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and …

This is another reason we are being careful with the correctness claim. The closest project I know right now that comes close to a formalized model of C++ is the BRiCk project: htt…

Yes, we were careful not to call it that. I still don't mind calling our programs verified, since they are verified in Rocq and we do our best to preserve the semantics of them. Ri…

Just like JavaScript folks like calling their compilers "transpiler", proof assistants folks like calling their compilers "extraction". Essentially it's a compiler from a high-leve…

We do C++ only because C++ is the primary programming language at Bloomberg, and we aim to generate verified libraries that interact easily with the existing code. More about our d…

We're based in NYC. The Infrastructure and Security Research team in the CTO Office, in particular. And we are looking for senior researchers to join us, see https://x.com/jvanegue…

Hi, I'm one of Crane's developers. You can map Rocq `bool`s to C++ `bool`, Rocq strings to C++ `std::string`s, etc. You just have to manually import the mapping module: https://git…

You're right about the records providing flexible order, I overlooked that. But Kip lets you repeat cases in arguments, so you're not limited to 8 arguments for a function. In case…

(bu tam-sayının) mutlak-değeri, (bunun 0'dan büyüklüğü) doğruysa, bu, değilse, bunun -1'le çarpımıdır. (5'in mutlak-değerini) yaz. (-5'in mutlak-değerini) yaz. You can try it in th…

Okay there is an updated web page and playground now: https://kip-dili.github.io/

Cases essentially act like named arguments, except the names are inferred from the case of an argument, which is inferred through morphological analysis. And that analysis can be a…

"fark" here takes two arguments, the first (the minuend) is in instrumental case (-le), the second (the subtrahend) is in genitive case (-in). Now, because of the suffixes of the c…

Yes, that's one of my inspirations! I'm writing a short paper about Kip and I'm citing Perligata there for sure. The closest modern non-English programming language I know that als…

That's okay, thanks for sharing!

It would actually be a good fit for event handlers...

That's pretty cool! From what I can tell, it does a morphological guess based on the suffix. If you didn't have the apostrophe, it'd have issues with ambiguity (say "aşı", does it …