Easy! that’s a simple multi-objective optimization problem!
56 karma · joined February 28, 2020
Indeed by sacrificing the power of type system we can augment classical axioms consistently as shown by HOL family.
These come with their own disadvantages.
Proof assistants aren’t whimsical like cottage industry of programming languages. Proof assistants are divided into 3 parts, the core or foundation (F) which is a very small language at the heart of the prover, the vernacular (V) the language in which humans write the code and the meta language for proof search and meta programming (M).
The V is translated into F and this translation is often proven to be correct. De Bruin criteria says that F has to be small and should be independently checked (mostly through inspection or mechanization in other framework). In Coq the proof derives is again checked from ground up by F when you write Qed.
Andrej Bauer explains better than I can.
https://mathoverflow.net/questions/376839/what-makes-depende...
At the core all these proof assistants, is a dependent total functional programming language.
Total means all functions must be obviously be terminating.
Dependent means types can dependent on values or more generally you can have quantifiers (sigma and pi).
Both Coq and Lean have variants of a dependent type theory called “Calculus of Inductive Constructions”.
Coq and Lean have tactics which can be thought of an embedded “proof language”. It’s an useful fiction because underneath it is just functions and inductive definitions.
Agda and Idris doesn’t have tactics, so the proofs have to be done through computation (by defining and apply functions and data types)
Lean and Coq differ in how they encode mathematical objects. Lean makes it much easier to make use of classical axioms. (Defining axioms is easy in both Lean and Coq)
From a more practical POV, Coq has the best documentation, books and development tools.
Lean has the WORST development tools of all 4. However has extensive libraries for mathematics. ( It is very painful to use )
Agda and Idris are about the same (set up is a pain otherwise about as good as Haskell development)
Even though Idris is marketed for “practical programming” it doesn’t have partial functions!!
I am not sure if Agda supports partial functions.
A more thorough comparison can be found here : https://artagnon.com/articles/leancoq
Their equilibrium population was over 100000!
I don’t think any sane regulator would ever approve such a system.. ever. The improvements are still too slow and corner cases still deadly.
On the hand the geo-fenced systems like Waymo, Baidu etc, might be difficult to scale are orders of magnitude safer. Perhaps better overall both short and long/term.
Yes I don’t know either but that’s my unconsidered opinion.
In New England Organic Valley is as good as it gets for store milk,
I thought clisp was maintained just to keep building Maxima
Look IITians are often entitled, opinionated and in rare cases obnoxious.
But never during my 5 years in IIT KGP, I have ever felt casteism among students and even amongst alumni after that.
Initially during freshman year there’s a slight sense of resentment against quota (affirmative action for lower castes) students but all of that evaporates as quota and non-quota students alike progress.
The whole point of getting advanced degrees is to shed the ignorance and discrimination and pursue what’s interesting, work with the brightest and of course make a better life for oneself.
Being casteist and discriminatory doesn’t take anyone far in life.
I really hope reports like these are media exaggerations and entitled casteist are very very few.
I have worked my whole life to ascend over this garbage. I don’t want this stupid discourse to follow me now!
No one wants to live in an overpopulated hellhole (aka India).
This should be lauded!
The foreign social media sites have political agenda blatantly well “foreign”.
Media houses are strictly regulated and have to abide much stringent criteria for reporting or an oped.
It’s about control it was in the best interest of these tech firms to be “neutral” before they captured the entire public discourse space. That is clearly not the case now, They have infinitely more power than they had before and even more power than the sovereign government in many many countries.
Some governments are trying to protect their (digital) sovereignty through regulation.
If one (adult) can’t handle drugs then help should be readily available as is for alcoholics.
No need to get political and emotional about it, there’s a pragmatic way.
They (Big Fossil) are not evil as long as they pay these “media” houses cozy bribe.
It’s mob rule at it’s most vicious.