Y
HN Search
Hacker News Search
new
|
comments
|
top
|
jobs
nikivazou
searching PlanetScale…
1.
▲
2.
▲
3.
▲
4.
▲
5.
▲
6.
▲
3 ms
·
1.
▲
by
nikivazou
10y ago
Liquid Types use the SMT solver to automatically generate proofs, while in Agda the user needs to manually specify the proofs. Also, Agda is a verification specific language, while (Liquid) Haskell is a general purpose language, which means
2.
▲
by
nikivazou
10y ago
It is like contract checking, but all the checks are done statically (at compile time) and automatically by the solver. Also, we allow the checks to only express things that the SMT solvers can decide fast (eg linear arithmetic). So, check