Anton Trunov

@ChShersh Objective Categorical Abstract Machine Language

What is OCaml? Wrong answers only

The work on Random Testing of a Higher-Order Blockchain Language has been presented by @ilyasergey at @icfp_conference in Ljubljana. Co-authored by Tram Hoang, @falsenov, and @LeoLambro. The paper: dl.acm.org/doi/abs/10.114…

@ciphernyx Very interested! Online would be great

@heades A naive approach that worked is to pretty-print a term and try removing pairs of matching parentheses one by one, parsing this back and checking the new AST is different. I'm curious to learn a better solution :)

@heades Nice! There is also one property I like to test: the number of parentheses the pretty printer generates is minimal. Not only this helps ensuring the result is easier for humans to read, but also, perhaps surprisingly, helped uncover a bug in the parser.

@gregory_malecha Had the same feeling a couple times when defining trees with complex invariants. I'm curious about your use case(s).

Now I find myself wishing #coq supported #inductionrecursion...

@CarlPatenaude @p_droabreu0 Let me just mention that the official plugin tutorial is here: github.com/coq/coq/tree/m…

@p_droabreu0 I'm also feeling the absence of intermediate and advanced Coq resources. What is the killer app for evars? How do I write a plugin? Are there consensus approaches to package management? Surely that information exists somewhere in the folklore.

You guys say what you want about Coq Ltacs, it may be painful sometimes but I honestly believe that this will still influence generations of metaprogramming languages. The ideas of managing the context environment programmatically and extensively is just too powerful...

@lambdabetaeta github.com/coq-community/…

PL twitter, is there a list of Coq/Agda greatest hits? Of course there's the Four Color theorem and Feit-Thompson, but what else could one list? CS examples welcome

@nate_yazdani @this_is_STR Congratulations Nate! Really excited for you

Exciting news: I’m joining STR (str.us) as a Programming Languages Researcher, working with their growing team of stellar folks in formal methods! @this_is_STR

As JetBrains we condemn the attacks taking place. Our hearts are with the Ukrainian people, including our own colleagues and their families.

If you're a user, a prospective user, or a learner of the Coq proof assistant, we encourage you to participate in the Coq community survey 2022: sondages.inria.fr/index.php/3563… (by 28 February 2022, AoE). We are grateful for all your feedback! 🐓✨👍

@ilyasergey Looks like Einstein's definition of insanity does not work anymore...

GitHub Copilot is terrible for live coding sessions: every time I show it in action on the same example, it generates different code. Neuro-symbolic gods work in mysterious ways.

@codydroux @mietek lmao

A great illustration of tactic-based theorem-proving as imperative metaprogramming.

@SandMouth FWIW, I always imagined sections and section variables as the closest syntactic analog to the typing judgment

The closest syntactic analog to the typing judgement `a : A, b : B, c : C |- f : F` in Coq is `Definition foo (a : A) (b : B) (c : C) : F := f.` The `f` and `F` are swapped and the symbols are wrong. It is always shocking how much symbols can throw me. Magnetic Field is B.

@oquechy [looking at the recipes in the IO monad] ;)

@falsenov Of course they do! But unlike imperative programs functional programs don't really describe the sequences of actions which are executed in the end. And much less so when the language is lazy

@maqstik Congratulations, Amrit! Warm wishes to you and your baby!

Had a baby today.

@intoverflow There was a discontinued attempt to introduce a linter at some point: github.com/math-comp/math…

@intoverflow I'd say it's kind of per-project in Coq, e.g. MathComp has a style guide for SSReflect-style proofs: github.com/math-comp/math…

Alas, no linter for Coq Some projects use shell scripts to search for easy-to-catch things (such as restricting usage of Require Export) But I haven’t found a comprehensive style guide, much less a linter/formatter (It’s hard! Would want to support Coq’s Notation feature…)