Hacker News Reader

Comment by adamnemecek | Hacker News Reader

This field is a killer app of coq. Nowhere else do your bugs cost more while the program size is small.

Someone at the Ethereum Foundation is working full-time on formal verification, and building a smart contract language to make it easier: https://medium.com/@pirapira/bamboo-compiler-started-produci...

"Currently I’m confident I can write an interpreter of Bamboo in Coq or Isabelle/HOL. I don’t want to expand the language much further until I write one so that I can prove properties of Bamboo programs. Ultimately I’d like to replace the compiler with a proven-correct one, but for that, a Bamboo interpreter needs to exist in a theorem prover."

I'm pumped cause this will popularize theorem provers and pump a lot of money into their development. There was that Stephan Diehl talk on the front page yesterday https://news.ycombinator.com/item?id=15582429 where he concluded that it's gonna be a while before see a language based on homotopy type theory.

He made a good argument. But these developments make me question whether crypto wont make them popular. This "early future" is kinda amazing.

Cubical https://github.com/mortberg/cubicaltt is a proof of concept programming language based on constructive (cubical type theory https://arxiv.org/abs/1611.02108) interpretation of HoTT.

Agda also added recently support for cubical paths https://agda.readthedocs.io/en/latest/language/cubical.html .

I'm also waiting on Lean https://leanprover.github.io to introduce cubical type theory for HoTT. Version 2 of the language had HoTT based on the univalence axiom which was dropped in version 3. With cubical type theory the univalence axiom can be constructively proved and is no longer an axiom.

It would take a lot of talent and time to use. It's why I usually push Design-by-Contract and/or runtime checks/tests. Far as new languages, you might find Noether interesting in how it is built in layers that let one trade verification difficulty vs expressiveness as desired.

https://github.com/noether-lang/noether/tree/master/doc/pres...

Among other interesting features. I recommend reading old one then new one.

I would imagine an idris derivative isnt all that much easier to write when compared with writing coq.

Oh yeah, Ive known people who could do model checking giving up on Idris since it was too difficult. What's interesting about Noether is it builds up from simplest models of computation to single threaded to distributed. The lower levels are like state machines. One could do that in languages for contracts working up from brute-forceable automata toward more expressive stuff that takes more work.

Plus, I thought you'd enjoy the language presentation as extra benefit.

Are we not confusing difficulty with familiarity? For me personally, as someone very familiar with FP, Idris was very approachable and easy to at least write simple proofs in.

I have nothing to say about the language (I gave up reading those cumbersome slides), but I am really amazed that you expect someone to like that presentation! :)

Proving theorems in Agda or Idris is like programming in more rigorous variant of Haskell. Proving theorems in Coq is... different.

I agree.

I do proofs and write small programs in coq regularly. I've spent most of my professional life as a web developer.

As with everything learning to do proofs and learning to use Coq are a matter of time, effort, and access to good documentation and other resources.

It is hard to imagine that a proof-assistant will be used as a tool for checking smart-contract correctness due to a lack of sufficiently trained personal. What this BC community is really need is a suitable programming language which will be tailored for functional correctness and expressiveness. Unfortunately, the Simplicity language addresses only the first half, and it is not sufficient for practical success IMO.

Reply on news.ycombinator.com